The Coq mailing list

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

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.  We might then call the 
simpler system "the specification"... but then often a follow-up proof 
shows a relation between that system and an even simpler one, so it 
really doesn't make sense to draw a sharp line between specifications 
and implementations.

Often a specific proof method or logical predicate will have a slot 
designated to hold "the specification," in which case it's sensible 
terminology, but IMO it doesn't make sense independently of that kind of 
context.

On 1/25/21 10:38 AM, Fritjof wrote:
> 1) implementation - as the *program*, collection of function definitions and 
> data types
> 2) formal specification - as the properties that argue about the program, 
> e.g., theorems, lemmas or axioms
> 3) constructed proofs - statements of the LTac language
>
> [...]
>
> Am I right, that the term *formal specification* often donetes the 
> combination of 1,2 and 3, or just 1
> or am I  missing something?