[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.

[densh]

Apart from prioritizing FFI (like Java/Scala, Erlang/Elixir), the other two easy ways to bootstrap an integration of a new obscure or relatively new programming language is to focus on RPC (ffi through network) or file input-output (parse and produce well known file formats to integrate with other tools at Bash level).

I find it very surprising that nobody tried to make something like gRPC as an interop story for a new language, with an easy way to write impure "extensions" in other languages and let your pure/formal/dependently typed language implement the rest purely through immutable message passing over gRPC boundary. Want file i/o? Implement gRPC endpoint in Go, and let your language send read/write messages to it without having to deal with antiquated and memory unsafe Posix layer.

[seanhunter]

Lean has standard c ABI FFI support. https://lean-lang.org/doc/reference/latest/Run-Time-Code/For...

[nudpiedo]

Literally the first line of the link:

“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“

My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.