3 ms·
>but that's beside the point It seems to me that it is an important point though. > Even a non-constructive proof of existence for x can be significant in a p
by constantcrying 4y ago
>but that's beside the point
It seems to me that it is an important point though.
> Even a non-constructive proof of existence for x can be significant in a programmatic context
Which has no relation whatsover to proofs and programms being the same thing.
- zozbot234 4y agoA type-level program is still a program. Non-constructive proofs are addressing the question "will this program crash or go wrong if I extend it to do X, regardless of how I achieve that?", which is exactly the domain of type-level programming.
- logarhythmic 4y agoPrograms and proofs are the same thing though according to the Curry Howard Correspondence, if I'm not wrong.