waynee95 (Oct 11 2022 at 13:20): waynee95 (Oct 11 2022 at 13:20):What's a good resource talking about how checking the correctness of proofs works in Isabelle?
Mathias Fleury (Oct 12 2022 at 05:05):It depends what you really want (how does the core work abstractly? how exactly? what should reviewer check in a development? HOL-Proofs?). Maybe @Lawrence Paulson's blog post on LCF?
waynee95 (Oct 12 2022 at 06:37):@Mathias Fleury
That blog post looks good. Basically I need it on a level where someone not familiar with proof assistants gets an idea why to believe machine-checked proofs
Lawrence Paulson (Oct 12 2022 at 10:42):Depends on how much detail you want. Possibly useful are this little example and this historical paper. One can also distinguish technical perspectives (formalisms and their properties) from informal ones (the ability to simply read a proof script).
Manuel Eberl (Oct 12 2022 at 15:50):I always say in my talks that internally, every proof gets broken down to the most basic logical inferences (such as modus ponens) and fed through a small kernel that only understands these basic inferences and is thus relatively trustworthy.
I think that's close enough to the truth to be valid for a talk to non-specialists.
waynee95 (Oct 12 2022 at 17:33):Lawrence Paulson said:
Depends on how much detail you want. Possibly useful are this little example and this historical paper.
I will take a look.
Manuel Eberl said:
I think that's close enough to the truth to be valid for a talk to non-specialists.
The context of me asking is that I am currently writing my bsc thesis where I formalized something in Isabelle and in the introduction/prelims after giving a bit of context on Isabelle and how the proving workflow works, I wanted to give a few words about why we can believe that if we proved something in Isabelle, then it's true.
Manuel Eberl (Oct 12 2022 at 17:50):Then perhaps also check with your advisor how much on that topic they want to have in the thesis. I would imagine some (e.g. theorem proving people) will think you shouldn't talk about this at all whereas others (e.g. non-theorem-proving people) will think it's very important.
waynee95 (Oct 12 2022 at 18:29):@Manuel Eberl Yeah, we talked about it. It falls into the latter case
Last updated: Dec 21 2024 at 16:20 UTC