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.