The Coq mailing list

[guillaume AT claret.me <guillaume AT claret.me>]

Hi,

There is indeed no documentation on what "verified" means on this project, I 
should add some!

I was referring to the file 
https://github.com/coq-io/opam-website/blob/master/src/Run.v with the 
definition:

```
Definition get_packages (packages : list Package.t)
  : Run.t Main.get_packages packages.
```

which describes the execution trace of the entry point `Main.get_packages` in 
a system with a list of packages `list Package.t`. The fact that this 
definition is well-typed shows that:

* `get_packages packages` is an acceptable trace for `Main.get_packages`;
* `Main.get_packages` returns `packages` in this case (the second parameter 
of `Run.t`).

I agree the "verified" term is ambiguous without any details.

Regards,
Guillaume

On 4/15/2019 8:52 AM, Théo Zimmermann wrote:
> 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.

Indeed there was no proof on the web-server, but this website does not use 
the Gallina web-server. It runs a Coq program every hours to generate static 
HTML files using the `opam` command to get the list of packages, and serves 
everything with NGINX.

On 4/15/2019 1:46 PM, Li-yao Xia wrote:> 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.
>>