The Coq mailing list

[1337 777 <1337777.net AT gmail.com>]

We at 1337777.net are also searching for such programmer, maybe we could concur with some joint proposal ?

One possible angle of view for this question :

Here is some profitable example of some new list widget for ur/web :

https://github.com/1337777/upo/blob/master/examples/listEdit2.urp

.. ur/web is the initial bridge for translating the old edition of mathematics instead as some hypertextual programming activity,

and the old wikipedia/git/ed with [branching for simultaneous editiong] is in fact old, maybe the new are towards xslt transforms with [linear-jumping-modulo for simultaneous editing],

 and the contrast of encyclopedia-style contra school/courses/timed-browsing-style is to be clarified,

and the obsession with coulds a-la- [ Clide of Martin Ring ITP2014 or HELM/MOWGLI of Unibo or edukera.com ] is maybe questionable, and the possibility of delivery of the computations directly to the clients computers a-la-ur/web is more profitable, this immediately signify that any such attempt shall start by identifying/delimiting some lightweight/minimal alternative to any theorem prover coq/dedukti/... (a-la- smltojs interface) or simple mathematics non-formalising writer ..!1?