HN user
Yeah, people always talk about the China "invading" Taiwan like PLA soldiers are going to be storming the beaches.
If I were Xi, I wouldn't do that; I would just blockade them. You can get the same capitulation (hopefully) without firing a shot.
Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future
The way I saw this proposed, back in the 2000s: "proof-carrying code."[0]
The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules.
Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof.
The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded.
With this news, I have to wonder how much longer bluray will live.
I hope that physical media sticks around. DVDs and Blu-rays often include something that digital releases don't: director's commentaries, "making of" featurettes, and other extras.
For me, it adds a whole new layer of fun to movies I already like.
Does the Mexican residency have to do with the AI stuff that the article mentions? Or just about making your retirement money stretch further? Or something else?
I’m surprised to not see more commentary on this one.
I agree -- this is big news, but the thread only has 21 comments?!
When the Trump admin kinda-sorta banned Fable a week ago, it seemed like it might be a one-off event: handicapping Anthropic because the administration has a grudge against them.
But today's news makes it seem like we're moving into a whole different world of AI regulation: each US model will have to be approved for release by regulators! And not only that, but the administration will whitelist who gets to use it "customer by customer." (Altman's words.)
Turning this essay into a song in the style of 2000's Hip Hop? It used to be hard
Have you listened to the song he links? It's very convincing. If you were just casually listening to it in the grocery store, you wouldn't notice it was made by AI.
Maybe "social capital"? https://en.wikipedia.org/wiki/Social_capital
The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver.
This reminds me of Dafny: https://dafny.org/
Actually, that's an interesting question: how good are LLMs at writing Dafny?
I'm very in favor of high-speed rail, in general. But I remember when the price tag had jumped to "only" $100B, and that was already considered a scandal.
At some point the state has to say, "our requirements are making it insanely expensive. We need to consider a different route, or a lower speed."
I wish the rules were trimmed down a little. I feel like there's a really lovely tight game under all the accumulated house rules and finicky stuff. And the existing rules tend to scare off newbies.
Interestingly, an experienced player proposed "Tibet rules," which are rules specifically for newbies that cut out a lot of the advanced mechanics: https://riichi.wiki/index.php?title=Tibet_rules&mobileaction...
The article is smarter than the title makes it sound. He's not seriously proposing that being rich makes you happy. And he notes that there's a big drop around 2020 specifically, which long-term trends don't explain.
Just to state the obvious: 2020 was the year of COVID, which played hell with peoples' social lives.
And I think it's been pretty well-proven that happiness is largely driven by the strength and quality of our social relationships. Anything that cuts us off from our friends, or prevents us from forming new friendships, is going to be visible in the happiness data.
Judging by the stats, we haven't dug ourselves out of the post-COVID hole yet.
Games ship with "6 expansions in box" which sounds great [...] until you realize that they're poorly playtested, lack balance, and add a confounding (and sometimes contradictory) number of rules.
Hot take: I have never played an expansion that I liked more than the base game.
It's interesting that you said "how to beat me." You also get better as you play the game more, right? So it could be you learning how to beat them ;-)
Agreed that Captain Sonar is awesome, if you can find 7 other players that are into it.
It's a rare thing: a real-time board game. No turns!
In support of Dominion: there are a million expansions that add new cards and mechanics.
It's very similar; they're all "social deduction" games.
I love the word "nerdgeist!"
Sure, there are lots of good lightweight card games. For example:
* Skull: https://boardgamegeek.com/boardgame/92415/skull
* Cockroach Poker: https://boardgamegeek.com/boardgame/11971/cockroach-poker
I'm thinking of breaking up with my local board game Meetup.
The reason why is: everybody there has board game ADD! I've been coming for 2 years, but we never play the same game twice; someone always brings the Hot New Game of the moment.
But I find that the first playthough is the least-fun one. That's the one where you're trying to remember what the grey cubes do, and whether they're worth victory points or not. And the game takes twice as long as it says on the box, because everyone needs to reason out their strategy from scratch.
I wish that I could convince my group to pick some set of N games to focus on!
What workflow do you use to backup Blu-rays? I was looking into this before, and I couldn't find anything convenient...
The US passed laws meant to limit marketing and overhead that tied insurers economics to the size of the overall medical bill... which means as healthcare spending rises, the dollars they’re allowed to retain can rise too, which basically means they're incentivized to drive costs up rather than down.
Yes, this is an important piece of the puzzle. The "medical loss ratio" for large insurers (the kind we all know and love) is set to 85%. So they can keep up to 15% of their revenue as profit.
As you said, if total spending goes up, they get 15% of a larger number.
I think the root problem is fee-for-service.
Doctors and other providers bill for each individual thing they do. But that means that their incentive is to do as much as possible, so they can quickly rack up billable codes.
It's like if developers billed their employer per line of code they wrote: the incentive is for churn, when it should be for slowing down and thinking about quality.
You are extremely close to arriving at the solution, which is medicare for all. Cover everyone, then almost noone uses the insurance except when they need it
Most Medicare recipients do get supplementary private insurance though? It's called "Medigap."
Medicare pays for 80% of patients' costs, but even the remaining 20% is a lot. (You get a $100,000 procedure -- you're on the hook for $20,000.) That's why people get Medigap coverage.
We can still have your employer provide a X% or $Y to an HSA account that the employee can buy health coverage wherever they like. (I'm not optimistic that this will ever happen politically)
Doesn't this already partly exist? My (US) employer offers an HDHP (high-deductible health plan) that comes with an HSA.
(It's not quite what you described, because you have to use the insurer that the company picked. I think you're describing something more like the Singaporean system with Medisave.)
I feel like this article ends just as it's starting to get going ;-)
In the COBOL modernization space, I want to highlight Mechanical Orchard[0]. Their analysis tools can trace the execution of individual jobs, and decompose a complex data flow graph into a series of nodes with inputs and outputs.
Once they have that, each individual node can be translated into a modern language, with every individual (input => output) serving as a sort of black-box test. That way, they can gradually rewrite a complex system, while ensuring that the semantics stay the same at each step.
(Sorry, I'm not sure if I'm using the correct COBOL/mainframe terminology, but you know what I mean.)
Hi Maximilian -- nice to hear from you!
I'm sad to hear that about LLMs. I sometimes wonder if the software world is going to be "locked into" our existing languages, because it's what the LLMs can work with.
FWIW, I think the PRQL syntax is beautiful.
Sure, but they never intended to support everything you can do in SQL. For example, they say on the Roadmap page that they're only going to support SELECTs -- there won't be a PRQL way to do an INSERT, UPDATE, etc.
Google's "pipe syntax" is a similar idea: [0]
It's not as elegant as PRQL, because of course it's bolted onto the existing SQL syntax, rather than a redesign from scratch. But it has a big name behind it, and it's actually running in prod in Google Cloud... so it might have more momentum.
[0] https://cloud.google.com/blog/products/data-analytics/simpli...
Is this project stalling out? The last post on the "posts" page is from March 2023. But the last commit to the git repo was last week...