Lean is lovely, but those of us using it for general purpose programming are a lonely bunch; virtually all discussion on Zulip is about mathlib and tactics (which is understandable).

I have heard of Lean, but I just took a look for the first time. Certainly, much more Idris/Haskelly than the OCamlish F*.

Are there libraries available for general programming in Lean? Can you compile to another lower-level language like C?

I would be interested in writing some embedded code that could formally be verified. Right now, I have put some time in to SPARK2014, the subset of Ada.

Lean in fact compiles to C so the C FFI is trivial to use. However, the only general programming facilities Lean has seem to be those required to bootstrap the language. I find it equal amounts funny and sad that you still cannot get the Unix epoch in Lean; you need to call the C functions through the FFI.

For verifying code Lean is not great right now (see a sibling comment in this post). For embedded code in particular, I remember there was a low-level formalizer, but I cannot remember what it was. This post here has many discussions and links: https://news.ycombinator.com/item?id=31775216

Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language)

But I was under the impression there was an almost assembly-level functional programming language with formal verification capabilities; I cannot recall it.

Thanks, I had looked at ATS many years ago, but I had forgotten about it. I'm going to look at both Lean and ATS, but I guess I'll stick with SPARK2014 for work now.