Hacker News Reader

Comment by jfoutz | Hacker News Reader

Lately I've been dabbling with lean. pretty tight vs code integration. I don't know why I keep getting pulled toward dependent types, like a damn moth to a flame. I get a little scorched, then, oh I should try ...

But yeah, compiler checked properties are something kinda magical. Even more when you can specify the property to check.

View on HN

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.

Reply on news.ycombinator.com