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