3 ms·

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 flam

by jfoutz 2y ago

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.

ykonstant 2y ago
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).
- eggy 2y ago
  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.
  - ykonstant 2y ago
    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 https://news.ycombinator.com/item?id=31775216 Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language) 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.
    - eggy 2y ago
      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.

by jfoutz 2y ago

ykonstant 2y ago

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

eggy 2y ago
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.
- ykonstant 2y ago
  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 https://news.ycombinator.com/item?id=31775216 Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language) 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.
  - eggy 2y ago
    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.