Lean is definitely a dependently typed ML-family language like Agda and Idris, so "ML" has it covered. And the long-term goal of Lean certainly is not "executio

Lean is definitely a dependently typed ML-family language like Agda and Idris, so "ML" has it covered. And the long-term goal of Lean certainly is not "execution is only secondary"; Microsoft is clearly interested in writing real software with it: https://lean-lang.org/functional_programming_in_lean/Programming-with-Dependent-Types/Worked-Example___-Typed-Queries/#typed-queries https://lean-lang.org/functional_programming_in_lean/Program... OTOH if you really want to emphasize "intended to express proofs" then surely Prolog has that covered, so Lean can be seen as half ML, half Prolog. From this view, the Curry-Howard correspondence is just an implementation detail about choosing a particular computational approach to logic.