Those are interesting approaches. I'm pretty pumped about Lean. It may just not have fit into his narrative and he can't talk about everything. Fstar and Lean a

Those are interesting approaches. I'm pretty pumped about Lean. It may just not have fit into his narrative and he can't talk about everything. Fstar and Lean are more children of Coq and ML (at least syntactically) to my understanding than they are children of Haskell. They're cousins. Although everyone influences everyone of course.