The Coq mailing list

[Fritjof <fritjof AT uni-bremen.de>]

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