The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

This is pretty cool to hear, I've been interested in seeing this kind
of research for a while.  I've always imagined that there would be a
lot of interactive proof visualizations that you could write on top of
coq so that as users did things in a theory's "native language" (e.g.,
dragging diagrams or clicking on postulates for basic geometry) you
could synthesize a coq proof under the hood.

I'll be interested to see what kind of tool you've put together.

Kris


On Sun, Aug 31, 2014 at 5:15 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> We're working on a novice-oriented interface at MIT.  I expect we'll make a
> public release in the next month or so.  However, you also might not be
> interested in a novice-oriented interface. :)
>
>
> On 08/31/2014 05:13 PM, Vladimir Voevodsky wrote:
>>
>> Hello,
>>
>> is there a working web interface for Coq?
>>
>> When I tried ProofWeb it told me 'Welcome to Coq trunk (Nov. 2006)"
>>
>> and then it refused to work at all (could not start a new line after the
>> first sentence).
>>
>> Vladimir.
>
>