lou1306

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.

Yeah I see now that P in the original post means a _property_, not a _predicate_. That clears it up :)

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?

> 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.

At some point Intel was experimenting a Xeon with built-in FPGA, maybe they were just a bit too early to the game :)

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.

Naomi Klein is the most vindicated nonfiction writer in modern history.

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".

> people who aren't able to write correct code are somehow able to write correct mathematical specifications

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).

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.

Ok there is a non-zero chance that they could face a lawsuit and get fined for billions, but that chance is not 1 either: there is always a chance they get away with it. And even if they don't, if in the meantime they farm 10- to 100-fold that amount of money by just breaking the law, it's still a no-brainer for them.

Norway (Yes this is a YAML pun)