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

On 11/12/16 22:57, Julius Michaelis wrote:
> So what are the tales you should be telling?
> On  3.12 20:53, Makarius wrote:
>> In general, the thm type in Isabelle is definitely not what is being
>> told in the common story about the "LCF approach", there is also not
>> "the kernel" in Isabelle. We need to stop telling these tales.

Reading the sources, reading papers, asking people who should know how
these systems are done, listening carefully. I do that myself when
talking to the colleagues behind the other systems (HOL4, HOL-Light,
Coq, ACL2, ProofPower).

The assumption that any of the LCF-style provers is 100% correct is
wrong -- that was never the case in last decades. If your work depends
on that assumption, you need to rethink what you are doing.

We need more clarity and more honesty.


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