[feral]

'Proofs' done by humans are done within a certain context; there's usually a lot that goes unstated, or is left unexamined at the finest level of detail.

Generally that isn't a problem and the 'small' details or assumptions don't 'leak' up to higher levels and do any real damage to the proof.

There's a movement to make proofs formally verified, to try move towards eliminating this issue, but that's hard, because writing out every little detail, specifying every last piece of context & assumption & step is laborious.

[cmdrfred]

> because writing out every like detail, specifying every last piece of context & assumption & step is laborious.

Can code be written and subsequently formally verified that can then help in the process of formally verifying code?

[tinco]

It is not the verification that is laborious, although it can be computationally intensive, it is the specification. It is making sure that whatever it is you are proving is actually exactly and completely what you desire of the function.

In this case the proof did not properly account for the full range of inputs, of at least skipped over the fact that in real hardware the integer domains are finite.

There's a lot of formal verification tools out there though, they do make it easier,easy enough to at least properly verify the correctness of a simple sorting algorithm.