3 ms·
Alas, not having had the time to fully read yet, but starting at the "Axiom rule" part, a strong feeling starts popping up that this is Lean, but with mathy sym
by groby_b 2y ago
Alas, not having had the time to fully read yet, but starting at the "Axiom rule" part, a strong feeling starts popping up that this is Lean, but with mathy symbols.
I don't know if the intuition will hold on further reading, but there was a strong "I've seen you in a different trench coat" feeling.
- rck 2y agoYup! Lean is based on a variant of the Calculus of Constructions, which is in turn based on strong connections between (intuitionistic) natural deduction and type theory. The connection is incredibly beautiful: https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions
- hoping1 2y agoAh heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!
- Tainnor 2y agoSequent calculus is way older than Lean or any similar such language. It's a bit like saying "this looks like Haskell" when reading about the Lambda Calculus.