When it comes to formal proofs of code, once you have a proof it is generally straightforward to verify (in the same way that you could for example evaluate a boolean expression). The problem is in finding the proofs - that's what requires labor and intelligence.
So the way I imagine it would work, is you tell a programming system which conditions the code it's going to generate should satisfy, and then it generates the code + proofs that it satisfies those conditions.
It might be trickier than I imagine though (e.g. for Chess/Go the reinforcement signal might be more suitable for learning than what you'd find with proofs).
So the way I imagine it would work, is you tell a programming system which conditions the code it's going to generate should satisfy, and then it generates the code + proofs that it satisfies those conditions.
It might be trickier than I imagine though (e.g. for Chess/Go the reinforcement signal might be more suitable for learning than what you'd find with proofs).
If you want to know more about proofs you might be interested in the series "Software Foundations" (https://softwarefoundations.cis.upenn.edu/).