AI is, apparently, very good at producing proofs. Formal verification of program properties was out of the reach of human labor, but may not be out of reach for 10 million instances of Claude. Software security will, by my estimate, just shift to this new paradigm.

My vague hunch is that in the next few years we (humans+AI) will rewrite the foundation of software to allow formal verification of all existing and newly written code, while keeping the same languages as higher-level abstraction.

Similar to Fil-C as a memory-safe implemenation of C. There will be formally-verifiable implemenation of C, C++, Python, Go, and so on. Not sure what that will look like, if it's even practically possible.

> AI is, apparently, very good at producing proofs.

Proofs of what? Defining the problem is the part that is hard, not the actual writing of the proof.

Do _you_ have 1e7 instances of Claude?

Cause this new paradigm sounds to me like "we checked, it's all good bro, trust me!"

how common are airpoane crash injuries?

Why do you think that matters?

Why would it not matter? Everything in safety culture is making the risks acceptable. Why does ETOPS exist when we could just disallow planes with twin-engine aircraft entirely?

The word you are looking for, probably, is "totally disconnected". Discrete always refers to the "discrete topology".

Navel gazing is a physical phenomenon, so if you would like to know everything about physical phenomena, you have to be able to predict the navel gazers.