I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking changes, and so on.
Some day, I'd love to write proofs instead of tests in some places.
I prefer F#/F* syntax, but I had to go with Ada/SPARK2014 for the safety-related control systems I am trying to verify formally and use for high-integrity applications. Rust is making some inroads with AdaCore and Ferrous Systems partnering on providing formal verification tools for Rust like they do for Ada/SPARK2014, but Rust still doesn't have a published standard like C, Common Lisp, Prolog, Fortran, COBOL, etc. Plus the legacy is immense for Ada and SPARK2014.
As someone only dimly aware of this space, I wish upfront they would highlight what they see as their relative strengths to similar systems and techniques. For example, I'm aware that both NuPRL and Coq have some ability to extract programs from proofs. What kinds of problems does F* do better at? Are there some areas where the SMT solver is a particular advantage? Are the extracted programs superior in some way?
Related. Others?
The F* Programming Language - https://news.ycombinator.com/item?id=31517176 - May 2022 (6 comments)
Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=25629058 - Jan 2021 (76 comments)
F* – An ML-like functional programming language aimed at program verification - https://news.ycombinator.com/item?id=15582969 - Oct 2017 (95 comments)
KreMlin: from (a subset of) F* to C - https://news.ycombinator.com/item?id=12753788 - Oct 2016 (2 comments)
Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=10949288 - Jan 2016 (28 comments)
F*: A Verifying ML Compiler for Distributed Programming - https://news.ycombinator.com/item?id=2663240 - June 2011 (9 comments)
They wrapped Dijkstra and Scholten's predicate transformer semantics [2] in a monad[1]! This almost irrationally pleases me. I'd really love the general concept to get wider traction too. While it's particularly useful for this kind of deep language design, a weakest precondition calculus be used manually when writing code[3] without any particular additional effort once proficiency has been achieved. To use an analogy, it's like the old trick of solving a maze by starting at the end and working backward. Often it ends up being considerably easier.
[1] https://link.springer.com/book/10.1007/978-1-4612-3228-5
[2] https://dl.acm.org/doi/10.1145/2499370.2491978
[3] It pretty much boils down to looking at your code and asking yourself "what has to be true for this to work?" and then writing code that ensures whatever is necessary is true for all possible code paths. Naturally that means limiting possible code paths. There's just one more reason why spaghetti code is bad.
The first thing that came to mind when I entered the site was the resemblance of the classic Soviet iconography to their logo, sans the hammer and sickle, then I checked the repo, and coincidentally, they have a recent commit (`c6fac4d`) titled "kremlin -> karamel" [0] ([...] a tool for extracting low-level F programs to readable C code*)... Apparently, the commit is one big rename operation from Kremlin to Karamel, funny.
F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
I'm curious how similar F* is to Lean Prover (which I've dabbled in).
I've never understood the relationship between F# and F*. I had previously come to the conclusion that F* was merely inspired by F#'s syntax and base-level semantics but that was where the relationship ends. As far as I can tell, F* is not a .NET language and doesn't run on the CLR. Is that correct? In the description it says it compiles to OCaml, which confuses me even more about the F* naming. What is the relationship to or level of interoperability with F#, if there is any?
We use F* for some of our crypto for embedded systems software :D
It makes me miss my time spent tinkering with Idris :)
Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my team was not.
I never really got to use it, and all I've ever done with it is a few of the toy examples on their website, but I haven't completely given up on it either. I think it's a much more approachable system than Coq or Agda, but still gives you sexy dependent types.
My PhD stuff is in Isabelle, and I do really like Isabelle, but I find that dependent types translate a bit more directly to "real code" than Isabelle's higher-order logic, so I would really like to utilize it for something, particularly with its .NET integration.