The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I agree that "specification" is too vague, imho one can still
recognize one reasonable use of it: In the industrial world I guess
the "specification", formal or not, is the statement that some
knowledgeable human reads and say "yes this is what we want for our
product". From this point of view the "formal specification" is what
lays at the frontier between informal and formal worlds.

Now when diving into the structure of a formal proof of course each
theorem is a formal specification followed by its proof. From this
point of view the question has no real meaning I guess: a formal
specification is a logical formula. Nothing really interesting here I
guess.

P.

Le lun. 25 janv. 2021 à 19:21, Milad Ketabii <ketabii.math AT gmail.com> a écrit 
:
>
> Hi Feitjov,
>
> When I was doing my PhD, I faced questions similar to yours. It emerged 
> from my encounter of HOL4 for completing a project after having used Coq 
> for another.
>
> Given your question is on the meaning of a word, I would like to refer to a 
> philosophical doctrine on how words acquire their meaning in a system of 
> signs. Using that doctrine, I put forward  how I came to an answer for 
> myself!
>
> So turns out that a text can be perceived as a construct made around 
> elemental "oppositions". Accordingly, textual constructs only produce 
> meaning through their interplay of DIFFERENCES (mostly emergingin in form 
> of binary contrasts) inside a system of distinct signs. This doctrine was 
> first introduced by Ferdinand Saussure on which J. Derrida drew for 
> introducing his notion of difference.
>
> Considering the above explanation, instead of hard wiring the words 
> "specification" and "implementation" to predetermined functionality or 
> referents, we can perceive them in a contrasting interplay whose connection 
> is established via the proof game. The "specification" is something used by 
> a "proof" to demonstrate "the correctness " of an "implementation ".
>
> Now going for the Saussurian doctrine, there is no problem for an 
> expression to be specification for an implementation,  but itself being an 
> implementation for something else. Therefore, I would definitely hesitate 
> to say it is meaningless (or even misguiding) to use the word specification 
> in the context of formal verification.
>
> Hopefully that was useful!
>
> Best
>
> On Tue, Jan 26, 2021, 2: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
>>