The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Getting to a place where .vo is platform/version agnostic, and where we have 
a decent library for checking/navigating .vo, would be FANTASTIC imho

Lots of benefits: checking untrusted code yes, but also integration into 
other software that might want to support loading of certified plugins (just 
for example)

Also would provide a clean way to combat bitrot by providing some forward 
compatibility to Coq-based projects

I presume I’m just rediscovering some of the thinking that’s already been put 
into this - thank you for your patience with me!

-t

Sent from my iPhone

> On Feb 2, 2020, at 2:44 PM, Emilio Jesús Gallego Arias 
> <e AT x80.org>
>  wrote:
> 
> Adam Chlipala 
> <adamc AT csail.mit.edu>
>  writes:
> 
>> I think this issue is actually relatively easy/cheap to sidestep. 
> 
>> Here's my solution, for an age when the world has converged enough on
>> a small set of proof assistants that are blessed for security-critical
>> verification.
>> 
>> [...]
> 
> Indeed, that sounds like a plan; of course work such as CoqInCoq
> etc... are also very welcome steps.
> 
> What I was trying to answer is more "is the current Coq implementation
> adversarial-resistant"
> 
> I think it not and it was not designed to be, getting a secure
> proof-checker will require new (and exciting) research and engineering work.
> 
> There is a danger IMHO in sending the opposite message.
> 
> Kind regards,
> E.