> I'd be stunned (and almost certainly dead at the time) if formal systems ever got to the point proved a program exactly met it's requirements. SeL4 (verified

> I'd be stunned (and almost certainly dead at the time) if formal systems ever got to the point proved a program exactly met it's requirements. SeL4 (verified microkernel) and CompCert (verified C compiler) are two such examples. [0][1] They're also both the result of a tremendous amount of work and have won international academic recognition, but still, it's not impossible for 'real world' code to be fully verified. > You see headlines about the costs of crypto bugs every week at least Nitpick: 'crypto' is an accepted abbreviation of 'cryptography', it's confusing to use it in reference to cryptocurrency. (Incidentally formal methods have been successfully applied to cryptographic code, but for whatever reason the most popular cryptographic libraries are unverified ones. [2]) > it seems completely lost on most HN commentators is crypto is at it's heart about building a world where all laws are written in software, assertions and promises the laws operate on aren't on paper and memories but rather can only be recorded in a blockchain, the judges are VM's executing code, and the jails have been replaced loss of crypto currency You're referring to smart contracts here, not to cryptocurrency in general. I don't see that it's lost on HN commentators, it's precisely the reason most of us dismiss 'smart contracts'. We have good reason to think that what they're aiming for cannot be done in practice (as you say, millions of dollars are lost due to small code defects), and that ordinary/real contracts are here to stay. I do agree though that if people are going to go with smart contracts, formal verification would be a useful tool. [0] https://sel4.systems/About/home.pml https://sel4.systems/About/home.pml [1] https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html [2] https://blog.adacore.com/sparknacl-with-gnat-and-spark-community-2021-port-proof-and-performance https://blog.adacore.com/sparknacl-with-gnat-and-spark-commu...