Comment by DonbunEf7

Programming languages from Adga to Monte are coming now with the ability to encode meaningful real-world proofs, and the compilers are checking those proofs.

We could be writing a lot of verified code, if we wanted.