[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Fri, Jun 04, 2021 at 11:05:42AM +0200, Tom Hirschowitz wrote: > [ 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. The difference is one of intention. Using axioms that do not compute is expected to not compute. Potentially crashing C++ code is at least intended to compute, and once mostly debugged, it mostly does. -- hendrik > > [Sorry I'm late on this one. This message was sent long ago but silently > rejected by the server, which I understood only later.]
