The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 1/25/21 1:03 PM, Michael Soegtrop wrote:
> > My opinion is that a lot of people think they agree on what "formal 
> > specification" means, but it actually means almost nothing and is 
> > best to avoid using! Instead, formal methods is all about proving 
> > connections between systems, often where one system is markedly 
> > simpler than the other and thus easier to build confidence in.
>
> I don't agree with this view. The specifications are supposed to 
> define desirable properties of a system, not how these are achieved. 
> These specified properties are those which a larger system requires 
> from a subsystem.
I think that kind of explanation only makes sense with respect to 
particular verification systems or even particular verifications. It's 
not possible, in general, to look at some code and answer "is that a 
specification or an implementation?".  I've come to see relational 
"specifications" as just programs written in a different language/style, 
with fundamental nondeterminism and lack of an obvious algorithm to run 
them directly.  That is probably the key difference in our perspectives.
> A specification of a C function doing minimization states that there 
> is a tuple of input parameters which may be varied and a goal function 
> which maps this tuple to a real number. One can then abstractly define 
> the minimum (or infimum) of the goal function over all possible 
> parameter tuple values. Then one can specify that the goal function 
> applied to the set of parameters the C function returns shall not be 
> worse than a well defined increase over this abstract minimum. Such a 
> specification has nothing to do with refinement, simplified systems or 
> possible implementations. It simply states what it means to minimize 
> something and what deviation from perfection is tolerable. In a larger 
> context such a specification is more interesting than stating that the 
> optimization function behaves approximately like some simplified 
> prototype algorithm. To the reader of the specification it tells 
> exactly what (s)he can expect from the C code. A comparison with a 
> simplified reference implementation wouldn't tell that, unless one 
> analyzes this simplified algorithm in detail. 

But your chosen specification here could easily be part of a refinement 
process that started with a broader specification, like maybe a set of 
differential equations for a dynamical system, from which you drew a 
connection to a particular algorithm and its associated helper 
functions, one that calls for computing a minimum within some 
floating-point tolerance.  I didn't at all mean to argue for executable 
reference implementations as the only appropriate kinds of 
specifications / intermediate steps in derivations!