3 ms·
These are actually the bugs I run up against the most often once #1 and #2 are dealt with: program functions as intended, but what was intended was wrong. Well
by crdoconnor 9y ago
These are actually the bugs I run up against the most often once #1 and #2 are dealt with: program functions as intended, but what was intended was wrong.
Well, that and "bug in dependency".
Formal methods are nice and everything but it's a massive waste of time if those are your main problems because you're doubling down on solving the wrong problem.
- virgilp 9y agoI wouldn't say "a massive waste of time" - except if done at the wrong level. I like Chris Newcorde's view [1] that TLA+ is "a pseudocode for writing design documentation". At that level, it's completely appropriate to use formal methods to check that you specified/investigated/considered all the edge cases. However, I find that using it to "prove program correctness" is indeed a waste of time, since what is most often wrong is your assumptions, not necessarily your implementation. [1]http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf