1. 14

  2. 3

    I think the key point from this is that there’s a flow:

    1. Informal specification
    2. Formal specification
    3. Formal verification

    If you have only an informal specification that’s still valuable because it lets people understand what they should expect from your code. From there, you can distil it to a formal specification. If you do that, then you have something that lets you reason about whether the design is correct, independent of the implementation. Taking a correct implementation as axiomatic, does the specification have the properties I want? If so, then the implementation may still be buggy but at least a correct implementation is possible.

    The final step, actually proving that the code is a correct implementation of the specification is probably too expensive for most projects, but it’s at least possible if you have a formal specification.

    1. 2

      Yes, I remember Plato’s Meno.