4 ms·
Formal proofs are a waste of time. You're more likely to make a mistake in the proof than in the code. How do you prove that the proof sets the right expectatio
by cryptica 5y ago
Formal proofs are a waste of time. You're more likely to make a mistake in the proof than in the code. How do you prove that the proof sets the right expectations? What is the point of proving that software meets certain requirements if these requirements are the wrong requirements and the problem was solved in the wrong way (the problem was solved, but it was the wrong problem; the user did not need that feature to behave like that)? Coming up with the requirements during implementation is the hard part; that's what most developers get wrong. Implementation is easy.
Formal proofs might even make software worse since they lock down requirements; potentially in a sub-par way. Not to mention that requirements change. Good code needs to be able to handle changing requirements.