F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
F* – A Proof-Oriented Programming Language
11–20 of 104 posts
Re: F* – A Proof-Oriented Programming Language
#12As 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?
I think humanity in general are only dimly aware of this space. The Research section is probably your best bet about what's different. I think your questions are what academics call "open".
Actually it does look like their book has at least some additional info in their intro section "To F*, or not to F*?"
The highlights seem to be:
- extensional equality (similar to nuprl)
- undecidable type-checking
- combination of both SMT and tactics, metaprogramming
- focus on compilation to mainstream languages, programming more than formalizing math
Re: F* – A Proof-Oriented Programming Language
#13Man, 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 te…
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-world use cases where this could really be applied?
Re: F* – A Proof-Oriented Programming Language
#14I'm curious how similar F* is to Lean Prover (which I've dabbled in).
Re: F* – A Proof-Oriented Programming Language
#15The 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 Karame…
I'm curious why the resemblance and homage to the Soviet Union in the first place, but I find it sad that people feel the need to rebrand things like this, to avoid the mob. Just because I don't like communism, doesn't mean people can't have things named after one of recent history's most well-known superpowers, with admittedly cool style.
Re: F* – A Proof-Oriented Programming Language
#16Man, 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 te…
Have you seen https://github.com/FStarLang/fstar-vscode-assistant? Copilot & F* works pretty nicely.
We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el
Re: F* – A Proof-Oriented Programming Language
#17I 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.…
> with AdaCore and Ferrous Systems partnering
I thought the partnership was already over? AdaCore left Ferrocene, and released its own support for a Rust toolchain lacking formal verification tools.
Re: F* – A Proof-Oriented Programming Language
#18As 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?
F* has an extraction backend which targets "human-readable C" code, contrarily to Coq which extracts proof to "machine-written OCaml" (typically the extracted code use a type-system-escape-hatch left in OCaml for the sake of Coq extraction). Consequently, part of the Everest project (the proven cryptographic primitives in particular) has been integrated into C code base like the linux kernel, firefox .
Re: F* – A Proof-Oriented Programming Language
#19Man, 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 te…
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-worl…
F* existed before Project Everest, but Everest did power a lot of its development.
We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/
Some of it is deployed in production systems:
* Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...
* Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star
Re: F* – A Proof-Oriented Programming Language
#20Man, 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 te…
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-worl…
The Everest project did publish a proved TLS implementation: https://mitls.org.
And at least the EverCrypt* cryptographic primitives has been used outside of academia.