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 worr

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