Hum, admittedly, most of this is past my knowledge graph, since I know nothing of mathematical logic. Are you saying the practical relevancy here is actually t

Hum, admittedly, most of this is past my knowledge graph, since I know nothing of mathematical logic. Are you saying the practical relevancy here is actually to logicians? In that it means they can now more easily come up with proofs for their theorems by simply writing a program instead of whatever more complicated paper proof they used to have to come up with? And that for software, it's only helpful in special cases where you need to guarantee a small piece of logic is 100% correct?