The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Sometimes the specification part of a formal verification project can be intertwined with the implementation. For example, Hindley-Milner style types (e.g, Haskell/ML) are a form of promise (formal specification) that a piece of code does something (e.g, returns an Int given an Int). It is possible to extend the type system in ways that makes this sort of specification more precise. You can do this using Sigma types and so on.

In some sense, Coq works in this manner. Just to clear up a misconception, Coq proofs are not all about LTac. The LTac scripts are essentially metaprograms that generate a term in Gallina, the same language in which you'd usually write the datatypes and function definitions.

On Mon, Jan 25, 2021 at 9: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