The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

There's some confusion here, perhaps all mine, about the distinction
between Coq as a system for verifying code (which it can do) vs. Coq
and the environment it runs in as a verified system (which it isn't).
It seems to me that these questions have been mixing those two very
different concepts.

Coq, merely by virtue of it being a system for verifying code, does not
enhance trust of itself and the environment it is run in being safe
to use to check that some other code can be verified.  One level of
trust does not eliminate the need for trusting the other level.

If you run Coq in a way such that something malicious can substitute
'echo "Qed!"' for your Coq prover without you knowing it is
doing so, then there is nothing Coq nor its developers can do to save
you.  Yet I am sure this must be obvious to all, so it must be me that
is still confused about your questions.



On Sun, 2 Feb 2020 15:50:27 +1300
Marco Servetto 
<marco.servetto AT gmail.com>
 wrote:

> > 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.