The Coq mailing list

[Ian Atol <iatol AT calpoly.edu>]

Hi Fritjof,

My understanding is that in the context of inside a Coq program, formal specification is mostly used as you say (the definition of theorems that we intend to construct a value to occupy - #2 on your list). But outside of that context, some refer to entire Coq programs as formal specifications, since they are a formal specification of the behavior of another program or some mathematical construct. 

Ian

On Jan 25, 2021, 7:39 AM -0800, 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