Comment by el_pollo_diablo
10 hours ago
I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.
For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved
{P∧B}S{P}
and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove
{Q∧B}S{Q}
or even
{P∧Q∧B}S{Q}
if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove
{P∧Q∧B}S{P∧Q}
which is incomparable and uselessly mixes both concerns.
You don't have to edit ("throw away") your original proof, it's just that a single proof covering the most precise description of the program's behavior is more compact than restating the program code a bunch of times plus the additional ceremony to assert that all those proofs refer to the same program.
> a single proof covering the most precise description of the program's behavior is more compact
Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form.
Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proof assistants that largely reduce the length of proof scripts. This is mostly a matter of tooling.
Yes, if you don't mind the repetition or have tooling to deal with it, you can have multiple separate proofs, dependent types won't stop you.