> A reliable system will need a relatively formal “proof” that what it does is correct.

One of my pet theories is that this is what programming evolves to in a few decades. Programmers write formal specifications for what should happen in some very high level language. AI + Compilers + ... take that specification, implement it, and prove that the implementation is correct and performant.

Think "SQL but not just for databases".