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

[Hendrik Boom]

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