How to ruin Linus's vacation
Posted Jul 20, 2011 3:24 UTC (Wed) by bfields
In reply to: How to ruin Linus's vacation
Parent article: How to ruin Linus's vacation
Well, it's also true that you can't write purely "formal" proofs for most mathematical theorems. And yet, mathematics gets done, because people can write perfectly good proofs in ordinary language.
And in fact anyone that writes non-trivial code probably does form in their head at least a hand-wavy proof of its correctness. If those actually got written down, it would probably help clarify thinking and avoid some bugs. But that doesn't happen for the same reason that nobody writes documentation.
An example of an exception: Documentation/filesystems/directory-locking.
to post comments)