Hacker News new | past | comments | ask | show | jobs | submit
socketcluster | on: Why writing correct software is hard and why math (alone) won’t help us (2016)
Exactly. I've worked on complex year-long projects where we've just been working non-stop, each team member generating thousands of lines per day and 1 year isn't enough to plug all the gaps in the spec with code and to cover all the exception handling cases at an MVP level.

You can't formally verify code when the code hasn't even met the spec yet! It takes a huge amount of time and effort to achieve this! Even when you think you've achieved this and your code meets the spec word-for-word, some stakeholders will still disagree based on technicalities and definitions!

How in the world are we supposed to prove that code is correct when people can't even agree on the same definition of 'correct'?! That's most of the work, really.

Also, if it takes people 1 year to complete a project in such a way that it barely just meets the spec to an acceptable standard, and only in a pure high level business sense; just barely covering all the basic exception handling scenarios; how long is it going to take to add formal verification on top of that? How many more gaps will have to be plugged, how many more assumptions will need to be enumerated, in order to make your formal proof air-tight? Then what happens if the client reads your formal proof and informs you that some of your assumptions are incorrect? What value is your proof then?

jdw64 | parent
I think our thoughts are similar. Sometimes I think like this: a craftsman choosing tools is important too, but ultimately the essence of a craftsman is what product they make — and I feel like people get too obsessed with choosing tools and focus on making the tool itself perfect.