The Coq mailing list

[Milad Ketabii <ketabii.math AT gmail.com>]

Hi Feitjov,

When I was doing my PhD, I faced questions similar to yours. It emerged from my encounter of HOL4 for completing a project after having used Coq for another.

Given your question is on the meaning of a word, I would like to refer to a philosophical doctrine on how words acquire their meaning in a system of signs. Using that doctrine, I put forward  how I came to an answer for myself!

So turns out that a text can be perceived as a construct made around elemental "oppositions". Accordingly, textual constructs only produce meaning through their interplay of DIFFERENCES (mostly emergingin in form of binary contrasts) inside a system of distinct signs. This doctrine was first introduced by Ferdinand Saussure on which J. Derrida drew for introducing his notion of difference.

Considering the above explanation, instead of hard wiring the words "specification" and "implementation" to predetermined functionality or referents, we can perceive them in a contrasting interplay whose connection is established via the proof game. The "specification" is something used by a "proof" to demonstrate "the correctness " of an "implementation ". 

Now going for the Saussurian doctrine, there is no problem for an _expression_ to be specification for an implementation,  but itself being an implementation for something else. Therefore, I would definitely hesitate to say it is meaningless (or even misguiding) to use the word specification in the context of formal verification. 

Hopefully that was useful!

Best

On Tue, Jan 26, 2021, 2:39 AM Fritjof <fritjof AT uni-bremen.de> wrote:

Hi,

I have a question regarding what formal specification exactly means in the
proof assistant context.

First *formal verification* means an implementation satisfies its formal specification.
The satisfiability is shown using formal methods of mathematics, e.g., a constructed proof
in Coq.

So we have the following terms:

1) implementation
2) formal specification
3) constructed proofs

In the context of proof assistants, e.g., Coq, I would describe:

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

However, I have also read that the implementation part is referred to as a formal specification:
- https://www.cis.upenn.edu/~bcpierce/papers/pierce-etaps2018.pdf

or the combination of 1,2 and 3 is referred to as a formal specification, like in: a program in haskell
is extracted from this formal specification.

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?

Kind Regards,
fritjof