[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.]
