What if the 'mathematical specification of its functionality' is incorrect? How to prove the correctness of the mathematical specification faster than the underlying environment, code and dependencies change?
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
Nothing forces developers to write a complete specification of the algorithm. You want to have it both ways.
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.
jongjong · · focus · HN ↗
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
imtringued · · focus · HN ↗
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.