In the context of programming languages, “proof” means “machine-checkable proof from mathematical axioms”. While there is difficult work involved in bridging between philosophy and mathematics, a programming language is only going to help on the math side, and on the math side, verifying proofs (once written in programming-language form) is trivial.
In the context of programming languages, “proof” means “machine-checkable proof from mathematical axioms”. While there is difficult work involved in bridging between philosophy and mathematics, a programming language is only going to help on the math side, and on the math side, verifying proofs (once written in programming-language form) is trivial.