> as very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
There is no contradiction here, TLA+ is mostly about proving properties of toy models, not end-to-end proofs about real programs. As TLA+ practitioners like to point out, the latter is only applicable to favorable "local" properties - this is what type systems do, they state claims that are quite aligned with the program's syntactic structure; or else to rather trivial programs where proving "whole-program" claims is still feasible. Even Verus itself doesn't really change this.
Isn’t the value in being able to verify the design before implementing? It would be more ideal surely to prove correctness of the deployed code, but I still find it very useful.
> It takes less time for local model to take the first action on your task than it does for Claude to validate your login, put you into queue and start issuing the commands.
This is only true if your local model is already resident in RAM / VRAM.
> They’re hyping up their products as being able to destroy the human race then are somehow surprised at the level of anti-AI sentiment out there in the world.
Yes, these are very clever fuzzers. But the real problem is not the cleverness, but the willingness to spin up 100s or 1000s of subagents no questions asked. Must make those token numbers go up!
It’s been more than a decade when CNN was a respected institution. I agree it’s too late for the news media in general. Their incentives are unfortunately all lined up just like social media: pure ragebait is the fully optimized product. The only thing changing from now on is fine tweaks to get it slightly more… ragey.
I'd roughly agree they are, but they have clearly positioned themselves in the opposite way as the mainstream media - the rest compete for ad-supported clicks and views; those two are fully paywalled and at a price that deliberately drives away anyone below say, the 90th percentile by income or wealth.
That resembles, to me, how newspapers used to be - except instead of a small fraction of people being willing to pay for quality news, roughly two thirds were (62 million subscribers out of 92 million American households in 1989 [1]). Like Bloomberg today, their incentives were to provide information for serious people and to cultivate a trustworthy reputation, rather than to enrage people into commenting and sharing articles.
The decline of newspapers is of course too much of a tangent, but I think it's interesting how the math kind of illustrates why most 'news' has to be trash now.
From what I can see, online media has finally taken over. The horrendous coverage from the 2024 election may have finally been the last straw for many people.
People seem to be focusing more on individual reporters, subscribing directly to good journalists who have gone out on their own. We are also seeing a thing that pleases me ver much: Reporters focusing on the subjects they are experts in and not doing a jack of all trades master of none. Its made me accept that I wont get top tier news in every subject so I have to pick what really matters to me(Tech, Food, entertainment, geopolitics of specific regions of the world etc.).
On the low end though its more bleak. TikTok slop, Youtuber "commentators" etc.
Static typing makes it easier to do RL targeting the sorts of things that static types encode, but it doesn't help at all with things that aren't really type constrained, like for instance writing accurate numerical programs.
I don’t think solving a millennium prize problem can be reduced to some DoorDash economics of “spent Y to make X.” What if it took someone their entire professional career to solve one of these problems, would it not be worth it by the same logic?
Surprisingly this is actually rather fitting in terms of time scale. When you consider it took ~10,000 agents 88 hours, or 880,000 hours to solve. That's 14.5 years in agent time of continuous 365/24/7 processing. Of course, humans solve things much more efficiently (and didn't also need the massive pre-training of every expert on the planet for 1,000,000,000 human years equivalent). But yeah, human researchers can solve a problem like this in a decade or so, while sleeping, teaching, traveling, and taking breaks, only working a few hours a day on the idea.
The entire controversy was that researchers were about to release their proof which OpenAI claimed to simultaneosululy discover. The proof is the researchers in question.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
reply