Re:F* – A Proof-Oriented Programming Language
by ykonstant on Thursday May 16, 2024 @05:42PM
(#40383608)
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
But I was under the impression there was an almost assembly-level functional programming language with formal verification capabilities; I cannot recall it.
Re:F* – A Proof-Oriented Programming Language
by eggy on Friday May 17, 2024 @06:25AM
(#40388317)
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.
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.