The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

I would say that, in a very strict sense, a "verified" program means 
only that some formal model of it has been constructed, and some 
properties have been proved about it. In such an absolute sense, the 
word carries very little meaning on its own.

Indeed, existing projects in formal verification vary wildly in what 
they model and how close the model is to reality, to achieve their 
diverse goals. So to make sense of what is actually verified, one has to 
read the details.

However, in today's world where "not verified" is the default, the 
"verified" label still sends a pretty strong signal, and if you assume 
that the authors are reasonable people, you can often guess the details 
to a large extent. So I think the word "verified" also carries a social 
connotation to be aware of.

Li-yao


On 4/14/19 6:20 PM, fritjof wrote:
> Hi,
>
> I have a question about what verified means in Coq.
> The coq.io/opam repository says: written and verified in Coq
>
> https://github.com/coq-io/opam-website/blob/master/src/View.v
>
> But I cannot see any Theorems in this repository:
> https://github.com/coq-io/opam-website/search?q=Theorem&unscoped_q=Theorem
>
> So the question is: what does verification mean in this context?
>
> Does the fact that something is written in Gallina also mean it
> is verified, as in dependent type verification systems, like idris or agda
> and theorems are only a way to proof more complex properties?
>
> Or do I miss something?
>
> regards,
> --f.