[tathougies]

These are interesting pros for lean. I just wanted to point out that Coq is also a programming language, and there are some packages of hackage of various data structures proven correct in Coq and then compiled from the original coq sources.

[agentultra]

I have read a fair bit about use of hs-to-coq and coq-haskell; Coq is a nice tool for sure!