Document the "software specification and development life cycle"

[shonfeder]

We should sketch out our hypothesis on the "specification life cycle", including notes on which parts we've been able to validate.

The cycle might go something like:

1. Exploratory modeling to understand problem domain
2. Exploratory specifying and testing to begin formalizing spec
3. Formal verification of specification to ensure expected properties of model hold
4. Implement spec
5. MBT to test conformance of implementation with the spec
6. Executable/interactive specs help onboard and guide new contributors and users in understanding system
7. Need for revision of implementation is identified
8. Exploratory alteration of spec to understand implications of changes
9. Planned change is formalized as revision to spec
10. Verify properties of spec still hold, revising if needed
11. Go to 4

graph TD
    expl[Exploratory modeling to understand problem domain]
    spec[Simulation and testing guides formalization of spec]
    veri[Formal verification of specification to ensure expected properties of model hold]
    impl[Implement spec]
    mbt[MBT to test conformance of implementation with the spec]
    onboard[Executable/interactive specs help onboard and guide new contributors and users in understanding system]
    needrev[Need for revision of implementation is identified]
    explrev[Exploratory alteration of spec to understand implications of changes]
    specrev[Planned change is formalized as revision to spec ]
    verirev[Verify properties still hold, revising if needed]

    expl --> spec --> veri --> impl --> mbt --> needrev --> explrev --> specrev --> verirev --> impl
    spec --> onboard --> impl

[konnov]

Who is it for?

[shonfeder]

• Us: to inform design.
• Users: to explain life-cycle of users.
• Potential users: to sell the value proposition.

[p-offtermatt]

I think something like this could be really useful, just to give people an idea of how Quint can offer value throughout this process - important to note that the value doesn't stop when the implementation is done, but that the formal spec is useful throughout the lifetime of the codebase, e.g. when making changes, when onboarding people, ...

I have some comments that may be less or more applicable. These are also just my current opinions, so there may be good reason not to take everything for granted.

1. I would like to put some emphasis on the top part of this lifecycle - maybe this is part of the exploratory modelling you have as the top node, or maybe it is even before that. Consider when the first line of formal spec should be written in this process. Is it correct to do formal models as the first step of the dev lifecycle? I think likely not. From my experience so far, there is lots of exploration that happens with English language docs and rough ideas even before it is worth considering writing models, when things are still heavily in flux, the design space is still large, etc. Many ideas can be dismissed without ever writing even anything more formal than a brief slack message, so at this stage (which might be dubbed something like "requirements engineering"), creating specifications does not seem like a good use of time.
2. At some point in this first stage, one or more candidate solutions should crystallize out as the most viable ones, and now it slowly becomes worth it to formally specify things. Now I think it becomes worth starting to model some of the candidate solutions.

Apart from that, I think the bottom "cycle" of the graph seems off to me - there's multiple cycles at least. During the initial development, there is probably a cycle that goes "Implement spec -> MBT -> Identify revisions -> Adjust spec -> Model-check spec -> Implement (adjusted) spec"

and then another cycle which comes after initial development, to deal with changes to the (finished) implementation that are necessary due to changed requirements. Here the spec is useful another time, because we get a "mini" version of the part at the top of the lifecycle - exploring the design space (now taking the existing spec as a basis, so modelling might be viable more early during the brainstorming process here). Something like Implement spec -> Requirements change -> Exploratory adjustments to refine the specification to match new requirements -> Model-check specification to verify it matches existing & new requirements -> Implement (adjusted) spec

These cycles maybe look similar, but what I want to emphasize is that the first spec might need to change as the implementation is done, just because we notice we cannot implement things as specified for one reason or another, but it might also need to change after the implementation is done because we need to change our system for outside reasons like changing requirements.

Hopefully my comments are somewhat helpful. Thanks for your effort in sketching this out!

[milosevic]

I am adding a link to this old repo: https://github.com/informalsystems/vdd for completeness as this was our perspective on this issue at that point in time.

[p-offtermatt]

Thanks @milosevic, I took a brief look, the repo looks interesting.

I think it would be amazing to understand how/if these views changed since then, and why - it would be super helpful to learn from and build on top of this.

[shonfeder]

This should include explicit mention of the use of quint as pseudo-code, which can take advantage of type-checking without needing a robust model for simulation.