|
What does source code/proof maintenance have to do with what remains at runtime? Sure, you can always extract the computational part of a program by erasing the logical parts, but that does not imply that code intermixed with logical parts does not create maintenance issues. Dependency management is one of those issues. Proofs require an acyclic dependency graph, in order to prevent circular arguments. By intermixing code and proofs, you force everything to fit in a single global dependency order. The point is not that it is impossible (it is possible), but that it is a maintenance nightmare. Sometimes you have to break an otherwise perfectly coherent module into smaller modules, just because you need to insert some other modules between them in the dependency order, that are only relevant to some minor proof. You have to constantly refactor your code as you reason on more aspects of your program. Have you already tested and certified your code and existing proofs? Too bad, your latest proof will require lots of handwaving and recertification to convince everyone that the big refactoring does not threaten the existing properties. Runnable code stands on its own, and should not be polluted with logical parts for every aspect of the program one may want to reason about. You can establish any provable property of a program using only basic logical tools: a single precondition and a single postcondition per function, a single invariant per loop, maybe dependent types, a few ghost values here and there, etc, and stuff all your reasoning in them in huge messy conjunctions mixing all the concerns together. That would be the equivalent of using nothing but a Turing machine to write a program. It is possible, it is theoretically appealing, but it does not scale. Software engineering is a thing for a reason. So is proof engineering. |