Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Safe to download and compile .v from evil source ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?


Chronological Thread 
  • From: Marco Servetto <marco.servetto AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
  • Date: Sun, 2 Feb 2020 15:50:27 +1300
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f68.google.com
  • Ironport-phdr: 9a23:STxxth0IxeVKx68msmDT+DRfVm0co7zxezQtwd8Zse0QLvad9pjvdHbS+e9qxAeQG9mCt7QY0KGK4uigATVGvc/a9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam4RvJ6g+xhbGpnZDZuBayX91KV6JkBvw+8m98IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QDtge+CRW2Ce/z1jNEmn370Ksn2OohCwHG2wkgEsoJvnvOttX6KKASWv2owqbW1zXDce1Z2Svh6IjPbxsspvSMUqhqccXNzkkjDRjFgUuKqYz7ITyVyvgNs2+A4upvUOKgkW8nqwVrrjezwccsj5DEi4QIwV7H7SV02Jg5KcG8RUJhYtOpEIFcuz+HO4dqWM8vQmJltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrmVOmLIDd4gGtpeLWjhxqv6ESgxOzxW8qu3FZFqSpFldbMtnQT2BDJ9seHTf598l+g2TaJyQ/T9vlJLV4omaffMZIswb49moANvUjeAiP6gkT7gayOekUh4Oeo6uDnYrv8pp+bMo95kgT+Pb40msOjBuQ0KBMOUHaB+eSiyrLj4VH5QLJRg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXfB0zIgZEVmCGLGULL/V+QuN7/gkJK+XaZULtSrhLNAq4vfviTkynlpLLvrh5ocedH3tRqcuGE6ee3e52o5dQ1dPhRI3SanRsHPHSSRaPi/gUKc15zV9A4WjX9+aG9KdxYeZ1SL+JaV4I2BLDlfWTCXtfoSAHvAQMWecfJ8nnTsDWrysDYQm0EP27V6o+/9cNuPRvxYgm9fm3dlx6ffUkEhrpzNxBsWZlWqKSjMtkw==

> Also: "put it in a container" doesn't address the other use case I
> mentioned above: namely, telling people that they can use Coq to certify
> the safety/correctness of untrusted code.

To make this more explicit:
if there was an online service that gives you "proven correct and safe code1"
and the corresponding coq proof code2; would running such proof be a
valid certification that such code1 is
correct and safe? or, is it possible that during the execution of
code2 arbitrary behavior makes a "yes" result even if the proof in
itself if bogus?
Note how running coq in a container or not does not really change the
issue here.



Archive powered by MHonArc 2.6.18.

Top of Page