Re:Software Foundations by Benjamin Pierce et al.
by pron on Tuesday December 15, 2015 @06:19AM
(#10737134)
> But there is a price to be paid, and that's the restriction to constructive logic.
That's the price on the proof side. The price on the program side is the need to encode complexity in the types because C-H is about abstract programs, not computations.
Otherwise, the existence of a computation is entirely ignored except where it may break the logic's consistency in the case of non-termination, but from the computation's perspective, a long computation and a non-terminating one are the same. The result is that you can "prove" the correctness of programs that are effectively non-computable, i.e. programs that don't encode effective computations (by effective computation I mean one that terminates before the end of the universe, but it could be exchanged with more practical definitions).
That's the price on the proof side. The price on the program side is the need to encode complexity in the types because C-H is about abstract programs, not computations.
Otherwise, the existence of a computation is entirely ignored except where it may break the logic's consistency in the case of non-termination, but from the computation's perspective, a long computation and a non-terminating one are the same. The result is that you can "prove" the correctness of programs that are effectively non-computable, i.e. programs that don't encode effective computations (by effective computation I mean one that terminates before the end of the universe, but it could be exchanged with more practical definitions).