The problem is most languages we use are not very safe, and which means if you have one unverified part in code, you can't prove code correct. I read a paper re

The problem is most languages we use are not very safe, and which means if you have one unverified part in code, you can't prove code correct. I read a paper recently which tried to do modular verification of C by adding runtime contracts are boundaries[1]. Theory wise its sound, but it's really slow. You may even have to rewrite code certain ways to make it perform better. [1] https://lirias.kuleuven.be/bitstream/123456789/471365/3/sound-verification.pdf https://lirias.kuleuven.be/bitstream/123456789/471365/3/soun...