[el_pollo_diablo]

Disclaimer: my shop develops non-trivial low-level software with machine-checked correctness proofs.

Rice's theorem implies that automatic static analysis (like Rust's borrow checker) will only get you that far. To go further, you must equip the program with a proof, which can be an order of magnitude more complex than the program.

Don't get me wrong, Rust is excellent for developing security-critical applications. Its borrow checker solves many memory safety and concurrency issues, and its type system more generally forces error paths to be explicit. The next step would be to use deductive methods to check that the error paths cannot be taken.

> make invalid states unrepresentable

That is a nice ideal, but not very practical. You need dependent types for that (for example, a sigma-type that bundles a value in a carrier type with a proof that it satisfies an invariant). They have their uses (e.g. at the interface of a library), but they are a pain to work with. You must build the proof terms together with the runtime values, thus entangling program and proofs into an unmaintainable mess. Oh, and forget about modular proof development: the dependent type encodes every constraint on the value, therefore most types must change across the program when you decide to prove an additional property of the program. You can't just keep the existing proof around and prove something else on top of it.

By all means, please keep some invalid states representable, and cleanly separate the program from its various proofs.

[zozbot234]

Proof terms disappear when you compile the program, they have no representation at runtime. They amount to compile-time-checked capabilities at most. So there's no real "maintainance" issue with entangling programs and proofs.

[el_pollo_diablo]

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.

[two_handfuls]

Maintenance as in, when you change the program you have to update the proof. This is easier if you can keep them modular.

[kldx]

If you don't mind, can I ask you a few questions about your tooling? I work in rust verification and would be interested in hearing about how industry uses verification techniques.