Just to add one bit: I find it curious that - proofs that may stumble on axioms are suspected of not being true programs, while - this would never happen to potentially crashing C code. [Sorry I'm late on this one. This message was sent long ago but silently rejected by the server, which I understood only later.]