Hillel

That’s completely true, but doesn’t really help. It’s just the minimum. The scale of project, goals, evaluation methods (are we done yet?), social/collaborative environment, etc, affect everything. Tighter constraints on how to plan, how to test & adapt, are critical

It helps in that it identifies the implicit goal we're seeking. Now we can make that goal explicit, and study it independently of the methods we've so-far used to try and achieve it.

eg one of the major benefits of formal specification is it's really, really powerful as a planning tool, but it's often (for many kinds of formal spec) useful _primarily_ as a planning tool without direct code connection.

Formally (i.e. mechanically) connecting high-level specifications to code is, unfortunately, intractable (at least currently) except in extreme circumstances. The question is, how important is it, really?

The ones you mentioned are all forms of refinement in a very precise sense.

that's interesting, could you please elaborate?

A refinement is the process of extracting a subset (and the converse of refinement, abstraction, is the process of finding a superset).

Even code describes a whole set of executables, as the compiler and the CPU are free to choose different behaviors as long as they are in the set of those allowed by the code (so the executable and executions are a refinement of the code, and the code is their abstraction).

Now, types, contracts and tests are a further abstraction, as they describe an even larger set of allowable programs: all programs that inhabit the type, those whose behaviors satisfy the contract, and those who pass the test.

All the techniques Hillel mentioned start with the abstraction, and so the process is one of refinement, i.e., starting with a large set of programs and narrowing it down (refining).