The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

Maybe Guillaume is reading this and will be able to be more specific,
but I recall attending his PhD thesis and it seems to me that he said
that he didn't actually have time to do any sort of verification on
his server written in Coq.

More generally, this shows that one must be very careful when people
claim a system is “verified” or “proven correct”. Just because it is
claimed doesn't mean that it is true, and when some stuff was
verified, it doesn't mean that it is what you actually care about. So
this is a claim that, by itself, doesn't mean much.

Théo

Le lun. 15 avr. 2019 à 00:21, fritjof 
<fritjof AT uni-bremen.de>
 a écrit :
>
> 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.
>