I don't think you can describe his beliefs using booleans like that: you have to use a numeric scale. It would be be correct to say: Elon would need a hell of a lot of ketamine to believe a colony on mars is a possibility.
Alternatively you may want to be a passive investor using the current rules for index inclusion, rather than having them altered to favor this loss-making trashcan on fire.
> The world seems to be fragmenting, into those that see the value in the latest from Google, and those that resist changes like this.
This reads as a strongly closed minded claim that has been "whitewashed into corporate appropriate speech" by an llm. If you cannot understand any validity to the other side of a debate then you are not engaging in discussion, no matter how your claims are dressed up.
with a mastercard from a swedish bank that is the experience that i get. all online transactions pop up a page from my back with qr code, this is authenticated through an app that shows me the transaction details and requires pin confirmation.
Dead code elimination is run multiple times, including after other optimizations. So code that is not initially dead may become dead after propagating other information. Converting dead code into an error condition would make most generic code that is specialized for a particular context illegal.
Nobody said one rack. Your entire rant is misguided. He analyzed what it would take to put one rack on one starlink like package in order to build a constellation.
The details might bury his point rather than illustrate it. The driving theme throughout seems to be that a tool tuned for correct syntax, with deep understanding of semantics will look like a Dunning-Kruger machine. The specific errors that the author's colleague was oblivious to don't add any weight to that general point, they only explain one specific instance. It's classic omega-consistency.
In addition both have a property similar to dispersion. In crypto each change to an input bit should cascade through as many output bits as possible. In ML each output bit should depend on as much of the input bits (and hidden layers) as possible. So they both feature a similar maximization of entropy.
> rollout will be incremental and it will self monitor by defining success conditions at rollout time.
This sounds a lot like allowing an LLM to define tests as well as implementation, and allowing the LLM to update the tests to make the code pass. Recently people have come to understand (again?) that testing and evaluation works better outside of the sandbox.
"in a wild or unsupervised state" seems like a particularly apt description of children. it does not seem to be derogatory: language really should be evocative as often as literal.
There are standard convex assumptions to handle incompleteness, decidability etc, i.e. the results are an over-approximation that terminates. Picking a approximation that is precise enough in the properties that you care about is part of the challenge, but it is an in-band problem. There are no hard edges between the theory and reality.
As with most engineering problems the out-of-band issues tend to be the hardest to solve. Models of the part underneath the interesting part need to be complete/accurate enough to make the results useful. Compare it to crypto where people do not usually try to break the scheme - they try to break the specific implementation of the scheme because the weakest points will be at the interface between the theoretical construction and the actual concrete instantiation of the device that it will run on.
The article describes fuzzing the library, this execution requires a program to be compiled. Typically fuzzing involves a minimal harness around the payload (a single call into the library in this case). There is clearly a bug in this program, and it does not exist in the minimal harness. It must be in the library code, which was covered by the proof.
The bounded, specific codebase that you refer to is typically the library *and all of its dependencies*, which in this case includes the Lean runtime. This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations. In this case the original gushing claim that everything was verified is incorrect and premature. The article seems like a good exposition of why.
There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it.
1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take).
2. It's the code in the binary that is executed (external view, that most users would take).
The key question does not seem to be "was the proof correct", rather "did the proof cover everything in the program". The answer depends on whether you are looking at it from the perspective of a programmer, or a user. Given the overly strong framing that the article is responding to - highlighting the difference in this way does seem to be useful. The title is correct from the perspective that most users would take.