> we’re in a business context where new features are ALWAYS more beneficial to the business inputs than formal verification.
Another way of framing this is "what is the impact (to the business / to the customers / to the users) of shipping a defect?". In a lot of contexts the impact of shipping defects is relatively low -- say SaaS applications providing a non-critical service, where defects, once noticed, can usually be fixed by rolling back to the last good version server side. In some contexts the impact of shipping defects is very high, say if the defect gets baked into hardware and ships before it is detected, and fixing it would require a recall that would bankrupt the company, or if a defect could kill the customers/users or crash the space probe or so on.
> In some contexts the impact of shipping defects is very high (…)
I agree however I think that many overestimate how frequent those environments are. Almost everything can be updated (and that includes dumb appliances with hardware chips replaced by technician) and the only real question is what is your reliability vector.
At the end of the spectrum there’s Two Generals Problem and Space Bit Flip and so much complexity that’s mind blowing. I’ve seen on my own eyes industry wide screwups that were fixed with month full of phone calls and paper slips exchange, so it’s not like we (as humans) cannot live with unreliable systems.
I’ve been researching formal verification for a while and IMO they are not fit for general use through lack of ergonomics. I might have some ideas how to solve it but I rather try to put in a commercial box <insert dr evil meme>
Things are often fixable, but if you keep breaking things for your user you're going to develop a reputation for being unstable and your customers will leave.
Bugs are on the spectrum - some might increase resource usage, or some might crash for a percent of users. Some might always manifest for specific cohort of users and it might not be profitable to fix it for them. It's an ocean of possibilities between "perfect system" and "complete failure".
Sanity test are degrees of magnitude easier than FV and they can assure at least that.
And even a "perfect system" might not be perfect for all users. I've seen lots of "old-school, battle-tested, rock-solid software" with bizarre behavior that supporters insist is an intended feature and can never be changed or configured, on account of it being convenient for some workflow back in the '80s or whatever. No system is so "perfect" that it can be all things to all people, unless it's truly trivial in scope.
Right but then it’s a requirement, the author frames the argument around FV when it’s NOT a written requirement
I mentioned exactly that:
> If a business requirement requires formal verification then the argument is also moot - because it is part of the business requirement - and so it’s not optional it’s a feature.
Another way of framing this is "what is the impact (to the business / to the customers / to the users) of shipping a defect?". In a lot of contexts the impact of shipping defects is relatively low -- say SaaS applications providing a non-critical service, where defects, once noticed, can usually be fixed by rolling back to the last good version server side. In some contexts the impact of shipping defects is very high, say if the defect gets baked into hardware and ships before it is detected, and fixing it would require a recall that would bankrupt the company, or if a defect could kill the customers/users or crash the space probe or so on.