I think Harper (who coined the phrase “computational trinitarianism”) doesn’t claim that “programs are proofs”, but rather that proofs are programs. That is, proofs should be written down in typed calculi and (to be intuinistically acceptable) should have computational content. But programming languages and type systems can be used for more things than just proving theorems.
I think Harper (who coined the phrase “computational trinitarianism”) doesn’t claim that “programs are proofs”, but rather that proofs are programs. That is, proofs should be written down in typed calculi and (to be intuinistically acceptable) should have computational content. But programming languages and type systems can be used for more things than just proving theorems.