2 ms·

I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statemen

by brazzy 2mo ago

I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statement: > Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel. I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.

inigyou 2mo ago
In every proof assistant something is doing all that logic, whether you call it a kernel or not. As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects). Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.