The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I've been watching research papers pop up on the topic since well beyond 
just 5 years ago.  It seems entirely plausible at this point that there 
are technical and/or social reasons that this intuitive idea just isn't 
worth the hassle.  We can at least say this goal has been "obvious" to 
the community for a while, so it's not a case of work only beginning on 
it when proof assistants reached a certain recent level of adoption.

In a typical open-source ecosystem of libraries, where library users 
sometimes feel compelled to contribute improved code to support their 
new use cases, it sounds like a mammoth liability to have to hop between 
proof assistants for different libraries.  We know how hard it is 
already to learn one proof assistant!

Even if a satisfactory translation between proof assistants is 
automated, it's likely to bring dependence on axioms that some users of 
the target proof assistant object to.  For example, many Coq users are 
accustomed to accepting excluded middle, but my understanding is that 
many data-type constructions in Isabelle/HOL work via a nonconstructive 
choice operator, and I don't think it's standard to assume such an 
operator in Coq (it's in the standard library but relatively rarely 
used), so that would be a genuine "philosophical" cost of importing 
Isabelle/HOL developments.  Conversely, I imagine modeling of nontrivial 
Coq dependent typing in HOL would be a nightmare, requiring a whole new 
set of skills to use an imported library effectively, even if its 
original code doesn't need to be changed.

On 5/29/20 11:36 AM, Abhishek Anand wrote:
> I'd like to understand why such a tool/setup doesn't exist.
> Because of technical difficulties?
> Because such projects won't be cool enough to publish in "top 
> conferences" and please the career gods?
> I very vaguely remember hearing about attempts to make such tools, 
> about 3-5 years ago. I'd love to hear their experience.