Comment by nudpiedo

I like a lot of the idea behind such theorem provers, however, I always have issues with them producing compatible code with other languages.

This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.

So no way of leveraging an existing ecosystem.