However the author never actually makes a good case for FV other than to satisfy hard-core OCD engineers like ourselves. Maybe the author feels like we all know their opinion - but it seems like the author is arguing against a poster of claude shannon.
If the system is - for all intents and purposes - deterministically solving the subset of problems for the customer, and you never build the state machine, then who cares?
My argument is “there isn’t one” — that’s provided we’re in a business context where new features are ALWAYS more beneficial to the business inputs than formal verification.
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.
Come to think of it I’m not really sure I’ve ever seen software created on behalf of a business, that has formal verification, where FM is not mandatory requirement of the application or it’s not a research project.
The last time I saw formal state machines built against a Formally Verfied system it was from a bored 50 year old unicorn engineer doing it on a simple C application.
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.
firesteelrain•2h ago
In most live production environments today, requirements do keep changing — security, compliance, customer behavior, scaling — even when teams think they're done.
Agile isn’t making an empirical prediction ("all requirements will mutate endlessly"); it’s a philosophical posture toward uncertainty
Wayne misses this interpretative nuance.
fredo2025•2h ago
I don’t agree on testing. It’s been a long time since I bought into that, and even tests for uncertain behavior to have confidence is a form of tech debt, as the developer that follows you must make a decision whether to maintain the test or to delete it; its value doesn’t usually last. An exception would be verifying expected behavior of a library or service that must stay consistent, but that is not the job of most developers.