I think this is the goal of proof assistants based on the Curry-Howard isomorphism, which the original author thought to denigrate for some reason.