> you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.

Having to do this is a sign that the new property depends on implementation details in some way. This can definitely feel like annoying busywork when there is only one reasonable implementation. Of course your sorting algorithm doesn't change the multiplicity of elements in the array, you wouldn't write a bug like that. Of course your sorting algorithm doesn't change the order of elements that are already sorted correctly, you wouldn't write a bug like... except unstable sorting algorithms do that and are widely used for performance reasons. So you do have to check your actual implementation step by step to verify that it really does what you think it must of course be doing. Trying to separate the concerns does not change this.

▲ el_pollo_diablo 15 hours ago | parent [-]

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.

▲

yorwba 14 hours ago | parent [-]

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.

▲

el_pollo_diablo 14 hours ago | parent [-]

> 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.

	▲	yorwba 14 hours ago \| parent [-]
		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.