>I would like to join the debate in a way that will vigorously stir the pot:
>
>When one wishes to plan a spaceflight for a planetary probe, the equations
>of motion for the planets, moons, and the probe are written down,
>constraints
>concerning the capabilities and objectives of the probe are written down,
>and
>the system is solved, yielding a mission plan that is optimal with
>respect to some objective function. Having generated the mission
>plan in this way, there is no question that the plan satisfies the
>laws of orbital mechanics. One does not generate a mission plan
>and then verify later that it satisfies the laws of orbital mechanics.
>Similarly one does not design an aircraft according to principles other
>than those of aerodynamics, and then later attempt to verify that it
>follows these principles.
>
>In the area of hardware and software development, one can
>either develop a system and then attempt to verify its correctness
>(post facto verification), or follow a path similar to the space
>probe mission plan (correctness by construction). Following
>correctness by construction, one might make specifications for the
>correct operation of the system, and then attempt to mathematically
>derive the implementation from the specification. There has been
>some research along these lines, including such languages as
>OBJ, CLEAR, and ML. What these have in common is that they
>rely heavily on a rather rich mathematical setting, namely category
>theory. There appears to be some sheaf theory creeping
>in as well.
Correctness by construction, or in other words the top-down development
of system and correctness proof together, also called refinement, is an
important engineering technique which is not limited to any specific
formalism such as category theory.
However I don't see that it need stir QED too much. Theories, mathematical
models, proofs are still needed. Top-down development is basically a way
of structuring the work that needs to be done, particularly so that the
artefacts developed are more amenable to being proved correct (i.e. to
satisfy their specification). There certainly are interesting implications
for proposing formalisms and proof paradigms which support top-down
development better, but this is just another example of the fact that QED
needs to be robust relative to differing choices of syntax.
John Staples