3 ms·
Lean. It's implemented in a dependently typed programming Lean is implemented in C++ [1, 2]. There's a message in there somewhere. The message is probably
by Cladode 7y ago
Lean. It's implemented in a
dependently typed programming
Lean is implemented in C++ [1, 2]. There's a message in there somewhere. The message is probably something along the lines of: if you want performance, use a low-level language.
[1] https://github.com/leanprover/lean/tree/master/src https://github.com/leanprover/lean/tree/master/src
[2] https://github.com/leanprover/lean4/tree/master/src https://github.com/leanprover/lean4/tree/master/src
- agentultra 7y agoI'm aware, I have a branch implementing C FFI for Lean 3; my point was that it's logic, mathlib could be implemented in system F instead. I'm pretty sure Lean could be implemented in Lean eventually.
- Cladode 7y agoWhat do you mean by "it's logic, mathlib could be implemented in system F"? System F is not dependently typed! Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things. [1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.
- agentultra 7y agoI think I mistyped. Pardon the pun! I meant that Lean, I think, could be implemented in Lean. Do you also work with Lean?
- Cladode 7y agoThat's an interesting question: can Lean be implemented in Lean's dependent type theory. I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.
- agentultra 7y agoThat sounds like it could be a lot of fun! Good luck. :)