2 ms·

Could you post some links on the soundness comment? I share a fellow siblings comment of a little skepticism? But I'm neither a professionally nor scholarly lo

Could you post some links on the soundness comment? I share a fellow siblings comment of a little skepticism? But I'm neither a professionally nor scholarly logician, though I've read and owned (a couple of times) Van Heijenoorts From Frege to Godel, so feel free to throw some meat my way if you follow up with this comment.

mafribe 11y ago
Well-developed proof assistants like Coq and Isabelle/HOL are the current pinnacle in scientific rigour. But soundness of a foundational system is always a worry and will always remain so. By Goedel's 2nd incompleteness theorem, you cannot verify absolute soundness. This is true for HOL just as for CoC/MLTT. However, Coq, Agda etc have a much more expressive logic, which is less well understood, and I think a couple of genuine logical breakdowns have been found over the years in Coq and Agda, see e.g. [1, 2, 3], but they could all be fixed. (I'm not following the development closely, but I think the Coq/HoTT implementation even seems to require patching Coq to disable critical checks.) I don't think that the HOL tradition has had to revise logical foundations. [1] https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... [2] https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.html https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.h... [3] https://coq.inria.fr/cocorico/CoqTerminationDiscussion https://coq.inria.fr/cocorico/CoqTerminationDiscussion
- dtornabene 11y ago
  this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdowns. I'm just slowly returning to this stuff through haskell. Heady stuff, that second mailing list post.

2 ms·

Could you post some links on the soundness comment? I share a fellow siblings comment of a little skepticism? But I'm neither a professionally nor scholarly lo

by dtornabene 11y ago

mafribe 11y ago
Well-developed proof assistants like Coq and Isabelle/HOL are the current pinnacle in scientific rigour. But soundness of a foundational system is always a worry and will always remain so. By Goedel's 2nd incompleteness theorem, you cannot verify absolute soundness. This is true for HOL just as for CoC/MLTT. However, Coq, Agda etc have a much more expressive logic, which is less well understood, and I think a couple of genuine logical breakdowns have been found over the years in Coq and Agda, see e.g. [1, 2, 3], but they could all be fixed. (I'm not following the development closely, but I think the Coq/HoTT implementation even seems to require patching Coq to disable critical checks.) I don't think that the HOL tradition has had to revise logical foundations. [1] https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.h... [2] https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.html https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00036.h... [3] https://coq.inria.fr/cocorico/CoqTerminationDiscussion https://coq.inria.fr/cocorico/CoqTerminationDiscussion
- dtornabene 11y ago
  this is fascinating! Thank you so much! I had no idea that the logic for Coq was more expressive, I can understand quite clearly how that can lead to breakdowns. I'm just slowly returning to this stuff through haskell. Heady stuff, that second mailing list post.