The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

> I would say that kind of easy classification only makes sense for a specific proof.

Real world systems have lots of proofs, lots of properties they must have. But we can form the conjunction of all those properties in a single type, which is "there exists a system S which has the properties P1 and P2... and Pn". That is the specification of the system S, and a proof of this spec is an implementation of the system S.

> The dependent type you selected could easily also be the implementation side of another verification

I'd rather say that we can reuse an implementation of a system as a part of another system's specification. It actually happens most of the time when we design new products : the first part of our spec is that our new product must be better than other existing products (otherwise, why publish the new one ?). That's section 1 of every research paper, the state of the art discussion. But still a spec is a type and an implementation is a proof of the spec. I can add the third leg of the stool : the verification that a system fulfills its spec is type-checking.

On Wed, Jan 27, 2021 at 1:39 AM Adam Chlipala <adamc AT csail.mit.edu> wrote:

I would say that kind of easy classification only makes sense for a specific proof.  The dependent type you selected could easily also be the implementation side of another verification, maybe starting from just asking for a number relatively prime to an input, without initially requiring that that other number be a full-scale prime itself.

On 1/25/21 1:16 PM, Vincent Semeria wrote:

Could we defend that the specification is the type, and the implementation is the proof ?

For example the theorem of decomposition into prime numbers,

forall n:nat, { p:nat, Prime p  /\  n mod p = 0 }

This is a type of functions in Coq, saying that for all natural number n, there exists a natural number p such as p is prime and p divides n. This can also be read as a specification : "for a natural number n, find me a number p such as p is prime and p divides n". And now the proof of this theorem is a term of the above type. If this term is coded in Coq without axioms, it is also an algorithm that computes the number p in question, so it is an implementation of the specification.

On Mon, Jan 25, 2021 at 6:13 PM Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

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

(or any other way to construct proof terms, by the way.)

I agree with your description above.

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.

In a stepwise refinement approach (which the DeepSpec project is, to some extent), the implementation of refinement step N is the specification of step N+1. 

 

Maybe code extraction / automatic code generation is not the best example of a refinement step, causing some confusion in terminology.

Hope this helps,

- Xavier Leroy

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