3 ms·
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinc
by inigyou 3mo ago
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinction between two kinds of things - "objects" and "types" - and then argue which one is better. No, I don't speak Lisp.
And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
- brazzy 3mo agoI 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 3mo agoIn 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.