|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Well, first of all, what Curry-Howard describe is not a proof (they
> call it a "constructive proof"),
why do you think a constructive proof is not a proof?
> As I elucidated, producing multiple distinct programs (that use
> different algorithms) shows it is not a compiler - it is not simply
> translating a program into another language.
Fine; so Curry-Howard systems are not compilers, for
distinct proofs of the same specification give different algorithms.
--
Alan Smaill
|
|