Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy



On 11/12/16 23:17, Makarius wrote:
> 
> We need more clarity and more honesty.

Hugo Herbelin is actually an expert an that.

Here is an example from a recent thread on coq-club "safe interface for
writing Coq plugins"
https://sympa.inria.fr/sympa/arc/coq-club/2016-11/msg00080.html (a
"plugin" is just an OCaml module produced by the user; in Isabelle/ML
that is trivial and does not need a special name).

That is an accurate and calm explanation of the realities of Coq,
without causing an uproar on the mailing list. Very professional.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.