Add glossary entries for "HoTT" and "kernel" #249
Conversation
Julian
force-pushed
the
hott-glossary
branch
3 times, most recently
from
b3e6b5d
to
1109836
Compare
templates/glossary.md
Outdated
| The goal of a proof assistant's kernel is to support all of the reasoning of the language with a small and bug-free, at the expense of expressivity or user-friendliness. | ||
| Specifically, the kernel uses a simpler but less featureful representation of proofs -- one a Lean user would normally not interact with, but which is intended to prevent the possibility that a bug allows invalid proofs to be accepted. | ||
| The user-facing portions of the Lean language are instead provided by its higher-level [modes](#mode), which ultimately are compiled into this internal kernel representation by the elaborator. |
There was a problem hiding this comment.
I don't love this description. It's not inaccurate to say that "input-Lean" is a different language from "kernel-Lean." "Less featureful representation of proofs" is more of a stretch.
I guess what's bothering me is that it presents input- and kernel-Lean as side by side? Kernel-Lean is 100% the "real" language, there's nothing very principled about the input layer. Input-friendly proof sketches go into the elaborator which tries to turn them into real proofs which can be checked by the kernel. Users do interact with fully elaborated proofs before those proofs reach the kernel, too; it might be more accurate to decouple the kernel from fully elaborated CIC proofs.
There was a problem hiding this comment.
Thanks for the feedback. I suppose I meant "expressive" rather than "featureful"-- I was trying to paraphrase Andrej's post:
The foundational system implemented in the kernel is too rudimentary to be directly usable for sophisticated mathematics. Instead, the user writes their input in a more expressive formal language 𝑉 (the vernacular) that is designed to be practical and useful. Typically 𝑉 is quite complex so that it can accommodate various notational conventions and other accepted forms of mathematical expression. A second component of the proof assistant, the elaborator, translates 𝑉 to 𝐹 and passes the translations to the kernel for verification.
But clearly I missed the nuances (and yeah featureful was a bad choice of words).
I'll try to give it another shot.
There was a problem hiding this comment.
@robertylewis I've neutered and reworked the kernel entry a bit. Can you let me know if you have any further suggestions on it?
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Julian
force-pushed
the
hott-glossary
branch
from
5c04e37
to
a60c24f
Compare
|
This looks like a good summary for the level its targeting! Thanks again, and sorry for sleeping on this for so long. |
No description provided.