for real formal methods it's a trade off that only those who really need security or reliability might practically make, eg banks and space agencies.

however, i think there is a continuum of methods, from TDD to proving correctness. it is often practical in the real world to do up front design before hacking out some code. i believe super smart hackers actually make lots of smart design decisions when "hacking" out code, whether that is realizing the appropriate loop invariants to make an algorithm work or figuring out the right abstractions for reusable code. there's lots of ways that good forsight produces correct code faster. that's what intelligence is: thinking, not brute force.

the smart coder, especially after gaining a variety of experiences and learning from different mentors, takes pieces of different methods in order to simultaneously make headway on different goals, not just correctness and extensibility, but refactorability, fast-rampup for new team members, fun, etc.

In my opinion, one of the big problems with formal methods is getting the specification right. You might be able to prove that your program conforms to your specification, but what is to say that your specification is any less buggy than your program? Some interesting work has been done with proving that certain errors do not occur, rather than proving the entire program correct. For instance, Microsoft's Terminator project [1] is used to prove that device drivers do not hang.

[1] http://research.microsoft.com/en-us/um/cambridge/projects/te...

I think that formal methods do matter, and can be realistic. We have a culture problem, perhaps inherent to the ease with which programs of unknown correctness may be written and executed, that usually we just don't care. How familiar is this cycle? iterate{think => type => execute => check}? Being rushed into the "protoduction" dev model doesn't help a lot either.

I had a professor who was apparently a student of E.W. Djikstra, and many of the points in this essay were essential to his courses. For example, exam questions weren't just "write code to do X", but "write code to do X and prove it", with failure to prove it resulting in a big fat 0. Of course, we were required to use weakest-precondition verification, from the bottom to the top. Not as tedious as it sounds, once you've gone through it once or twice, and I think the point wasn't to teach something we would use day-to-day, but to teach us that verifying programs by hand was not only possible but tractable. It seems like the TDD movement kind of makes the same point, though perhaps less formally.

Another professor introduced a variant of this technique developed for verifying the critical points of parallel and multi-threaded computation, which while far more tedious has been vastly more useful in my career as a model for thinking about concurrent programs [not bulletproof, of course, because runtimes and hardware sometimes do unexpected but perfectly valid things with our programs].

Most algorithms, at their core, have formal descriptions short enough to prove by hand in a matter of minutes. For those parts, I think it's realistic to use formal methods. All the other cruft we tack on to our programs to make then flexible, perform in a variety of contexts, handle varying data types, error checking, etc.; I think those fall in the realm of what you describe as "realistic programs", and which amounts to a daunting heap of code to verify by hand. Luckily, we can again follow his advice and use computation as an alternative, and verify by hand a program which can verify some or most of our work for us -- that seems to be what a lot of static analysis is all about.

I don't know. Do you ever run into situations day to day where you find yourself verifying your code by hand? That's usually what happens when I get deep into finding an error.