Sure, TLA+ lets you verify whether P is true in every state of every behavior by checking []P. But a _counterexample_ to that property, if it exist, is _some_ state in _some_ behaviour where P is false. Thus, if your model checker proves []P false, you have indirectly proven E<>!P (where the initial E means exactly "for some behaviour").

Going back to the example, "proving that a game is winnable" should be achievable by model checking the invariant "the game is never winnable" and failing. Or am I missing something here?

First of all the initial definition is totally correct, and if your embedded function needs to call an intermediate layer to access the hardware that layer is an OS. Second of all, all those "purposes" are exactly achieved by providing _managed_ access to hardware resources.

And that is valuable in whatever world we end up living in. Sure, 10 years from now my bank app and my Hacker News browser may both be written by "my LLM" and tailored to my use cases and desires. Will I want them to share memory? I don't think so.

In this case, while the Apple Concert Hall may superficially look like just another music venue (many of which are privately owned in their own right, obviously). But its musical programme will almost surely follow a different set of guiding principles, in conformance to how Apple wants to project their brand to consumers. And the goal itself of hosting live music performances takes second stage (heh) compared to that of marketing them for streaming consumption. Speaking of which: it's not mentioned in the article, but I would be _extremely_ surprised if Apple didn't make this move with Vision users in mind.

This is literally the opposite behaviour compared to what is written in the source code, even when you "assume the infinite loop terminates".

This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s

> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself

I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.

> the mathematical spec would get completely invalidated every week or so each time you did an update

Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).

> She is no less democratically elected than the prime minister of a parliamentary republic

Well I would say this is arguable. Sure, her power is ultimately resulting from a popular mandate. But, if your country elects the head of state directly (say, France) then there are two "hops" between a popular mandate and the head of the EC. Whereas, if you are in a parliamentary system, it's three "hops" (MPs -> head of State -> EC president).

Of course, the same applies to whatever remains of Twitter now.

For a more extreme (although somewhat inverted) version of this, see Zeeman. He spent years trying to find a knotted sphere in a 5D space. Then realised this was impossible and got a proof for it in a few hours. [1]

[1] https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

> probably you do not need to do any of that.

Indeed, I find that at least in my case, on a pretty average Intel machine these checks add very little overhead, especially compared to the benefits. I do not really understand how the examples in the blog post can get 100% (1st one) or even 10% (2nd one) faster.

(And yeah, I know that the obvious solution is to develop these tools in C/C++: I am just exploring the capabilities of Go in that space).