The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi Fritjof,

If you put everything in Coq, it makes it harder to see the separation and blurs the lines.

For example, in the case of using Coq & VST (https://vst.cs.princeton.edu/) you have:
- Implementation = your C code
- Formal Specification = your Hoare tripple which also includes the functional definition of the function.
- Contructed proof = the proof of your Hoare triple correctness.

Personally I would argue that piece of software generated from a formal specification are not "verified" but "proven by construction/synthesized", as opposed to an existing fragment of code that is later verified to match the formal specification.

Do note that a formal specification does not necessarily have to be originally written in Coq, e.g. RFC 7748.

Kind Regards.

On 1/25/21 4:51 PM, Ian Atol wrote:

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