> That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages But proofs are wr

> That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages But proofs are written in systems of logic and programs are written in (programming) languages, so if there's a correspondence between the first there really ought to be a correspondence between the second!