> If programs were easy to prove correct This is just another turtle layer because such proof is only vs a "specification", which turns out to also be a progra

> If programs were easy to prove correct This is just another turtle layer because such proof is only vs a "specification", which turns out to also be a program, written in another language.