Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
- To: Julius Michaelis <j.michaelis at liftm.de>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
- From: Makarius <makarius at sketis.net>
- Date: Sun, 11 Dec 2016 23:17:59 +0100
- In-reply-to: <20161211215724.GA22532@liftm.de>
- References: <email@example.com> <firstname.lastname@example.org> <20161211215724.GA22532@liftm.de>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
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