Of course, if you sneak in a simple patch that an AI agent wrote for you, nobody might notice. The fact is, maintainers of big OSS projects are increasingly dealing with patches in the 10kLOC range, all at once, coming from people with little to no previous engagement with the project: that's usually a dead giveaway.
Uhm, I can see the desire to simplify, but the passage about "reachability" sounds odd.
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?
You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.
A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.
Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.
On top of what Andrew said, "failure as reachability" is a property of the implementing model checker, not the formalism itself! If you convert "we can win the game" to "it's not true that always we haven't won" and write that up as a TLA+ formula, you get `". But that means "we win in every behavior", aka `<>won`!
> It’s not simply to “provide access to hardware resources”; plenty of embedded systems do that with runtimes that have no business calling themselves an “OS”. No, the core purpose of a modern operating system is to partition different applications off from each other, and carefully control how they can communicate.
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.
Well my comment was half in jest, but No Logo talks at length about the encroachment of megabrands into everyday life, and the replacement of the "public sphere" with controlled spaces that conform to the brand's image.
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.
Entirely different situation. Polymarket is a gambling website and is subject to regulation. In Italy and (I think) Spain, they may shut down connections to a Google Cloud or AWS server _at the IP level_ if they have a _suspect_ it's hosting an illegal streaming service. This may effectively black out entirely legitimate Web sites with _no_ correlation to sports.
Yeah the argument here is clear, also rather silly. Either you must accept that your language allows for completely useless computation, or, if the compiler is so good at detecting "unreal programs" it should also refuse to compile them.
I can understand adding the 'unreachable' function to the object file, I can even understand plugging it into the final executable, what I (and most other people) object to is making it the de-facto entry point.
This is literally the opposite behaviour compared to what is written in the source code, even when you "assume the infinite loop terminates".
That's the problem with UB, once you hit it (or even have it in your code), you can't really trust anything about the execution anymore. That the function is called isn't something the compiler does on purpose, it's just that the main function is compiled empty due to the UB and the function directly behind it is executed because the CPU just keeps looking for the next instruction.
To be frank, it is a quite eccentric way to appoint an executive leader: imagine POTUS being chosen by state governors.
> 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).
O(1) insertion is the amortized worst-case time complexity, actually. (Amortized in the sense that the O(n) cost of copying is paid only during the n-th insertion). Average complexity is a slightly different thing.
It is not “worst-case” (as the post demonstrates, you can get worse results by using specifically crafted data that exploits hash collisions). There are algorithms that can get you O(logN) instead of O(N) even on such data.
reply