coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] verified or not verified

From: fritjof <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] verified or not verified
Date: Mon, 15 Apr 2019 00:20:19 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=SoftFail smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-phdr: 9a23:ZGOqiRQdokMyPgnLJ3phpCCIktpsv+yvbD5Q0YIujvd0So/mwa6yZBKN2/xhgRfzUJnB7Loc0qyK6vmmAzxLucnJ8ChbNsAVD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN7s9xgHXrnZLdOha2WFlLk+Xkxrg+8u85pFu/zlMt/4768JMTaD2dLkkQLJFCzgrL3o779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWMtaSi5PDZ6mb4YXAeQPPfhWoZT+qVQBsRSxGBKhBP/zxjJSmnP6wbE23uYnHArb3AIgBdUOsHHModX7LqcSUPy1zKvPzTXNcvhb3jn96JLJchA9o/GMWrxwfNHMyUkpFgPJl06fqZb7MDOQyOsNtXKX4Pd+Wu+2jWMstg9/oj+qxsg2i4nJgJoYxUzD9SVg2oo1JNq4RFZ0Yd6lDJtQtzyaOJBsTsw+RGFovSA3waAFt56jZCUG1ZoqyhHFZ/GDcoWE+A/vWeKMLTtimX5oe7Kyiw6x/EWi0OHwS9e43VhQoiZYkNTBtWoB2wHO5sSZTPZ2412v1iyV1w/J7+FJOUA0mrTfK54m2rMwkpwTsVraEiLyhUn6kaybe0U+9uiz8OvreKjpppGfN491kA3xL7ohltS+AeQ+LAcOQ3CW9fmy2bDs50H0RLRHgucrnqTdrZzWP9kXq625DgNN14Ys8Re/DzOo0NQCmnkHKUpIeBydj4joJ1HOIvf4DfmkjlSxljdrxunKMab7AprTK3jMjrHhcaxg5EFC0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m24MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5jM0ADWUNsEJqQvbrlF+FXxZOYXf3Vbgx4zw9To6rW9SQDruxiaCMiX/oVqZdYXpLXwjVTSXYMr6cUvJJUxq8Z9d7m2VZB6WnSsorzxyruQm8x7c1drOFqB1djorq0Z1O38OWkBgz8TJuCMHEjjOQSWAxlHkFQjIwmqxy8xcklwWzlJNgivkdLuR9ovNEVgBgb8zYyfI/WomrCl+HZd3PRFilQ5OqDGNpQw==

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.

[Coq-Club] verified or not verified, fritjof, 04/15/2019
- Re: [Coq-Club] verified or not verified, Théo Zimmermann, 04/15/2019
- Re: [Coq-Club] verified or not verified, Li-yao Xia, 04/15/2019
  - Re: [Coq-Club] verified or not verified, guillaume, 04/15/2019