Re: [TYPES] What's a program? (Seriously)

[ 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.]