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.
The trade off you speak of rely on the unspoken assumptions that (0) applying formal methods costs more than not to, and (1) the astonishing complexity of our programs is actually needed.
I highly doubt (0), at least when you take into account the costs of errors: crashes, wrong results, security breaches… These costs impact the user instead of the programmer, but they are costs nonetheless (plus, letting customers pay for these strikes me as not nice).
I highly doubt (1), at least when you take into account our overusing of low level programming languages, and of course anthropomorphic thinking.
Comments
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.
The trade off you speak of rely on the unspoken assumptions that (0) applying formal methods costs more than not to, and (1) the astonishing complexity of our programs is actually needed.
I highly doubt (0), at least when you take into account the costs of errors: crashes, wrong results, security breaches… These costs impact the user instead of the programmer, but they are costs nonetheless (plus, letting customers pay for these strikes me as not nice).
I highly doubt (1), at least when you take into account our overusing of low level programming languages, and of course anthropomorphic thinking.