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" (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.


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