A 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.
Re:The Mathematical Hacker
by logarhythmic on Saturday December 24, 2022 @12:39AM
(#34114318)
Programs and proofs are the same thing though according to the Curry Howard Correspondence, if I'm not wrong.
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.