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.