I'm talking about hard problems. A proof for such a program you suggest is trivial and probably not worth knowing. A program is a proof that there exists a type

I'm talking about hard problems. A proof for such a program you suggest is trivial and probably not worth knowing. A program is a proof that there exists a type which satisfies a proposition. Not all propositions are interesting and neither are all programs.