I feel like Wayne is taking the Agile Maxim “requirements always change” too literally. Agile doesn’t mean "every requirement always changes forever”.<p>In most live production environments today, requirements do keep changing — security, compliance, customer behavior, scaling — even when teams <i>think</i> they're done.<p>Agile isn’t making an empirical prediction ("all requirements will mutate endlessly"); it’s a <i>philosophical posture toward uncertainty</i><p>Wayne misses this interpretative nuance.
The diversion through phase changes is awkward, here? I would use that metaphor to point out that many of the properties and requirements to maintain one phase are not relevant when in another phase. More, some properties become harder with different phases. Sure, holding water is generally easier than holding steam. Neither is easy at large scale, of course.<p>I think you could stick with construction metaphors for a lot of learning. Scaffolding key stones is particularly instructive. You will build a large structure that is intended to be torn down in order to build another structure. And there is basically no avoiding it.<p>I'm not clear how to move those ideas to formal methods. Typically you do that by keeping different layers that you formalize to different degrees? Along with processes to confirm compliance at the different layers.<p>Software seems to get tough as we often wind up trying to expand solution and construction models to be fully inclusive of each other. We don't necessarily do this for any other construction. Do we?
Preface: A Formally verified end to end application with associated state machine(s) is kind of my engineering holy grail - so I’m a likely mark for this article.<p>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.<p>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?<p>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.<p>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.<p>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.<p>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.