| |||||||||||||
How to ruin Linus's vacationHow to ruin Linus's vacationPosted Jul 20, 2011 3:24 UTC (Wed) by bfields (subscriber, #19510)In reply to: How to ruin Linus's vacation by smurf 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.
(Log in to post comments)
How to ruin Linus's vacation Posted Jul 20, 2011 4:05 UTC (Wed) by viro (subscriber, #7872) [Link]
Yeah, well... you forgot to add "and actually read" to conditions... Exhibit A: people adding hardlinks to directories or equivalents thereof, despite the aforementioned example of documentation ;-/
We do need such writeups, of course. If nothing else, writing them tends to find holes - see e.g. ->d_lock mess discussion on fsdevel lately. There the locking order had been fscked in head (not transitive, for one thing), but locks outside of that set had mostly avoided bad trouble. Trying to write the proof of correctness hadn't been fun (and what I've got still relies on unverified assumptions about the things filesystem code does not do; verifying those has already caught a bunch of really broken things), but it helped to catch rather nasty stuff. Simply by reasoning about the properties of counterexample - i.e. "what would a deadlock have to look like". It's math, like any other...
FWIW, I wonder what backgrounds people have - in my case, it's geometry and topology and _that_ has certainly helped to acquire many mental habits useful for that kind of work...
How to ruin Linus's vacation Posted Jul 20, 2011 23:02 UTC (Wed) by bfields (subscriber, #19510) [Link] Yeah. Especially for CS students, something like the classic first point-set topology course might give good experience with that kind of proof-or-counterexample mode of problem solving. I think that's rare, unfortunately, at least outside a few countries with very rigorous math programs?(Like some others, I'm a refugee from mathematics, coming late to this after getting a PhD (commutative algebra and some algebraic topology). Not a particularly smart career path, but fun in its own way.)
|
|||||||||||||