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)

Of course it is not to everyone's taste, but Ikea definitely has an aesthetics. A Lack coffee table or a Poang chair are instantly recognizable.

I also have a fine experience, but only by switching to the For You feed full-time and mostly sticking to my compsci-academic-tech-programming neck of the woods. Minority or not, the users GP mentions are so obnoxious that it affects the 'vibe' of the platform as a whole. Look up any "Top Posts" tracker/feed/whatever. No matter that I even (mostly) resonate with the underlying political leanings, I find the tone pretty dreadful.

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

Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"

> he had spent the entire weekend trying and failing to prove it. I, on the other hand, had put all my energy into finding a counterexample and had one within an hour.

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

Better at Go for automated reasoning tools, this means quite a lot of array lookups within tight loops. I asked because I noticed some AI agents quickly want to jump on the "eliminate all bounds checks" wagon as soon as the low-hanging optimization fruits have been picked, and it takes some hard data to put some sense into them. My question really was: is this kind of preliminary profiling enough, are there other pitfalls of arrays/slices in Go I am missing, etc.

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

> Another lesson that Americans have already learned is the peril of excessive financialization of the economy

Don't mean to be blunt, but when did that happen? How has a country where you can finance your burrito [1] "learned the perils of excessive financialization"?

Also, a lot of this (especially the slower recovery after 2008) reads more as the perils of being the periphery of an empire vs being the core.

[1] https://finance.yahoo.com/markets/stocks/articles/uber-techn...

Question from someone trying to get better at Go: _before_ going all in with unsafe pointer operations, would it make sense to write a function harness & profile it with/without the -B flag to determine the actual impact of bounds check?

Sure, but those were likely bugs in the compiler's codebase that in principle could be isolated and fixed. With an LLM there is no bug and there is no fixing procedure: all outcomes are context-driven and (more or less) nondeterministic by design. I don't mean this in a dismissive way, but there is clearly a difference there.

Oof that's not a good look. You can trivially avoid this by just prefixing all variable names with a salt. By the way this (or a variant thereof) is called "avoiding unwanted name capture" if you want to sound all sophisticated :)

> it's more of a problem that it's so heavily dominated by US politics.

I agree the default Discovery feed is not great, but you can just switch to a different feed like For You or the recent Eurosky version of it, called 'fu'. It vastly improves the experience.

What about a "fake push" that does not leak message contents, sender etc.? Fuzz the time the push notification is sent by a random amount of time and you have something plausibly private given the constraints?

Is this the old "breakdown of the bicameral mind" theory? I don't know. I think that tin trade routes breaking down + rise of iron-wielding civilisations are more plausible.

"The EU" is a loose term. At least in _some_ cases (such as this one), the Parliament has shown more attention to the voters. I'll concede that the deck is stacked against it, but this reflects a common trend in the West of overpowering the executive branch at the expense of the representative bodies.

That makes perfect sense indeed, although personally I'd prefer two senators per state. But since the EU as a political union is an afterthought of an economic union, it's full of loose ends like this. Also, national governments will be very reluctant to give up this kind of power.

The Council must go at some point. It is a "legislative" body... composed of members of the _executive_ branch of the individual countries. Granted, that's not the only problem with EU governance, but it is a rather glaring anomaly in terms of transparency and accountability.

Furthermore, at least in the case of Italy & other parliamentary systems, there's something like 3 levels of indirection between the people and their "representative" in the Council:

People elect members of the Parliament -> MPs decide who is the Prime Minister -> PM decides who sits in the Council

We should likely just replace it with either a "EU Senate", where each country elects the same number of senators, _or_ a chamber with truly European elections (as in, every EU citizen may vote for any candidate, regardless of their nation). But the latter option seems still out of reach as of today.