Math is about clear communication between people first and foremost. That's why Shinichi Mochizuki's claimed proof of the ABC conjecture isn't accepted - he's unable to communicate it to enough mathematicians to get a consensus on its validity. LLMs generating Lean proofs are basically following that same schema. Sure, something has been proven. But what? Where's the clear communication explaining it to the satisfaction of other mathematicians?

Do I fully believe all of the above? Not exactly. But compiler authors do. Does it make a really good argument to never use C or C++? Yes. If only we had 50 years of optimization work in any language with better semantics.

To be clear, Google was doing this out of self-interest. Paying user ISPs for access to those users is not a cost they want to pay. But it's the same as any other protection racket. A local shopkeeper has personal reasons to not want to pay off the mob, but that doesn't mean their position is wrong.

But yeah; don't join the military.

Try checking in only your prompts and nothing else. Just the parts you actually typed. See how well it works to regenerate the same application next week, let alone next year. Prompts are fundamentally a different sort of thing from code. Do not mix them up.

Assembly makes non-local reasoning mandatory, as any code can update any location in memory without restriction. All memory accesses are global. References need not even be by name - they can be via computed addresses. There are no restrictions in place allowing the structure of the program to provide boundaries on what pieces of code may be understood as units.

This isn't some slapdash random patching. Everyone involved knows that assuming that the λ in λCDM is a constant is shaky. It could be a function of time, or even location in some way. But it's simplest if it's a constant. So you start by modeling the universe as if it is. Then you determine what sorts of observations would support or contradict that, and you start making them. When you get results, you start examining what version of the model best explains those observations. And someone somewhere goes off to try find a better model than any version of λCDM. If they succeed, their model will eventually supplant it. This is how science progresses, even if the experiments are less under the control of the experimentors than they'd like. The important part that you make revisions in response to observations.

(FWIW, particle physicists are constantly frustrated that they can't find counterexamples to the Standard Model. They know it has to be incomplete, but the lack of contradictory observation leaves them no direction to try to improve it.)

I honestly am curious. I've seen a few examples presented for it, but they always seem like bad software engineering to me. Where's an example that does something in a cleaner way than alternatives present in other languages while remaining compatible with local reasoning?

I don't think raw machine code (not even assembly) is the best form to reason about program logic. It just takes too many steps to execute sophisticated processes to keep them all in your head at once - or keep them all in an LLM context at once.