F* – A Proof-Oriented Programming Language

by montyanderson • 2 years ago

236 102 2 years ago

tombert7• 2 years ago

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.

jfoutz2• 2 years 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.

ykonstant6• 2 years 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).

onhacker• 2 years ago

After C#, I learned F#, I loved language structure, but I was not able to run it on production effectively.

A language isn't enough, a language recognized from its support in ide/production and community

tombert7• 2 years ago

I didn't find F# so hard to run in production, particularly after JetBrains released Rider, but even before that I didn't think it was so bad.

At Jet we managed to get to pretty decent scale with F#, and for the most part got pretty ok performance. Often I would use the C# versions of libraries simply because they were updated more frequently. Everyone says that the C# interop is clunky and I think that's just not true, I found it relatively easy to work with C# libraries and utilize the .NET Framework. I used ConcurrentDictionary and SemaphoreSlim pretty heavily, for example. For the stuff was a little cludgy, I found it pretty straightforward to simply make wrapper functions that did what I needed.

I even found the object-oriented support in F# to be pleasant, though I didn't use it a lot. The syntax was really terse but easy to read, so in the rare cases where I had to extend a class or something, it wasn't hard. If I needed to implement an interface, it was also pretty easy to write an anonymous interface and plop that into a wrapper function.

One thing that I didn't like about F# was the kind of unpredictable performance with the async monad. It was hard to measure, and it didn't seem to work completely deterministically due to some kind of laziness that I never completely understood. The task monad released a bit later seemed to fix that, but that was integrated a bit later than my time at Jet.

Still, I found it a pretty decent language, to a point where if I started a company I would genuinely consider utilizing F#.

williamcotton• 2 years ago

Ionide, The F# language server, is excellent.

I use F# in .NET Interactive Jupyter notebooks daily at work and it works quite well.

The community around the language is very helpful and the Discord is great for all sorts of issues ranging from beginner to advanced.

I love the Fable compiler which targets JS, TS, Python and Rust and makes for a wonderful way to share a domain design across multiple code bases.

daxfohl2• 2 years ago

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?

lambdanik3• 2 years ago

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

octachron2• 2 years ago

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.

lambdanik3• 2 years ago

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

tombert7• 2 years ago

I have not tried the VSCode stuff, but I did try the Emacs thing. Looking at the repo you linked, it looks like the first commit was last year and I left Jet in 2018.

The Emacs mode was fine, I didn't think it was bad, but it was still a tough sell to my team; none of them wanted to install Emacs, they wanted a Visual Studio or JetBrains experience. I'm aware that's an uphill battle, and maybe it would be a different story if the VSCode extension existed in 2018.

toasted-subs• 2 years ago

Where do you even find orgs that let you program in those fun langs?

University jobs?

tombert7• 2 years ago

I was working for Jet.com, it was one of the very few places that did F#. The reason I was hired was because I had Haskell experience from working at NYU as an engineer before.

barrenko• 2 years ago

There are some trading companies as well, I guess because it's ocaml adjacent.

happypumpkin• 2 years ago

Maybe try looking for Clojure jobs? They aren't super common but are a lot more so than any other lisps or functional languages that I'm aware of (except maybe Scala).

abeppu2• 2 years ago

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?

jfoutz2• 2 years ago

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

abeppu2• 2 years ago

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

octachron2• 2 years ago

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 .

eggy4• 2 years ago

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.

letmeinhere• 2 years ago

My understanding is that the key feature of SPARK is design-by-contract aka run-time enforced pre- and post-conditions plus invariants for loops. Whereas F* lets you define dependendent types, a subset of which are compile-time constraints similar to those SPARK contracts. Is that a fair contrast?

Jtsummers• 2 years ago

Fairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html

SPARK's pre-/postconditions and assertions can be statically checked, they aren't just for runtime enforcement. This is its key value proposition, if it were just runtime enforcement it'd be nice, but not that great.

debugnik3• 2 years ago

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.

eggy4• 2 years ago

Very well might be the case. I am speaking on old news. I would guess the lack of an official published standard makes it hard to create tools and support them over time - a moving target.

pelagicAustral2• 2 years ago

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.

0: https://github.com/FStarLang/FStar/pull/2489

seanw4442• 2 years ago

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.

mapcars• 2 years ago

Agree, and there are other projects with fun names like https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation)

debugnik3• 2 years ago

I'm guessing they came up with the wordplay before the invasion, and then regretted it because the reference suddenly stopped being purely historical.

And I get it, I've been phasing out this username, which I picked with bad timing, to avoid unintended connotations, even though I was simply thinking of Robotnik and not anything russian. I've got nothing to do with their language, so it just isn't worth it.

wisemang• 2 years ago

Well tbf Kremlin (as typically used) isn’t just a USSR reference it’s a specific place in Moscow. Still used as a metonym for Russia’s government.

That said I do actually love that Soviet propaganda aesthetic. Can appreciate not wanting to be associated with the existing madman running Russia though.

unstruktured2• 2 years ago

F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!

wk_end2• 2 years ago

Correct me if I'm wrong (I've only dabbled in F* and only briefly read about 1ML) but wouldn't F*'s full dependent types make 1ML redundant?

That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexities they bring.

unstruktured2• 2 years ago

Interesting point. I never inferred a strong connection between dependent types and the unification of records and modules. Maybe a real PL theorist around here can provide insights on that subject.

joshmarlow• 2 years ago

I'm curious how similar F* is to Lean Prover (which I've dabbled in).

slushy-chivalry• 2 years ago

and both are backed by msft?

bmitc• 2 years ago

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?

samueldurante• 2 years ago

I believe that F* is named purely for marketing purposes, or perhaps to specify another programming language with syntax derived from OCaml.

But other than that, I don't think it has any other relation.

lambdanik3• 2 years ago

Not just marketing ...

About the name: https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-h...

mkehrt• 2 years ago

I'd assume both are named after System F, the Simply Typed Lambda Calculus enriched with a variety of types of what would widely be called generics.

mkw5053• 2 years ago

It makes me miss my time spent tinkering with Idris :)

User23• 2 years ago

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.

0823498723498729• 2 years ago

looking at your code and asking yourself "what has to be true for this to work?"

Wait a moment: are there people who write and ship code without continually asking this question, at least to handwaving precision?

chuckadams2• 2 years ago

They internalize it with tacit assumptions and let runtime exceptions deal with it when the assumptions are violated. We all do this to some extent, and not just in programming, but many people are a lot more YOLO about it when the language allows it (see “duck typing”)

vinnyvichy7• 2 years ago

It takes effort for me to compute whether grandfather is de gauche or de droite.. the better question to ask yourself continuously is whether: does this noise (spaghetti/imprecision in this context)

improve or remove performance ((0-1) though the 2 questions are related; it's enough to point out that if necessity is the mother of invention, then paradox is the father of discovery)?

(0-1)

https://quillette.com/2022/04/05/noise-a-flaw-in-human-judgm...

https://www.newscientist.com/article/2431131-buildings-that-...

6gvONxR4sf7o2• 2 years ago

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.

bluGill2• 2 years ago

While I agree with that in principal, in talking to people who have actually written proved programs I get the impression they don't think it is practical to prove programs that are more than medium sized. I'd love to prove my code correct, but I deal with 10s of million lines of code and nobody has a clue how you would approach a problem that large (we use C++, but you can select a different language if you want - the problem is the size and you can't get around that with a different language

PhunkyPhil• 2 years ago

Surely it wouldn't be aimed at proving a 10 million line black box of code, right?

In my mind it would have to be built from the ground up, sub unit tests for function proofs and maintain 100% coverage as you go along. As long as the constituent parts are proven you don't have to zoom out to a macro level.

Someone• 2 years ago

Divide and conquer does work a bit, though. Languages that support strong encapsulation of various structures will be easier to work with than those that pass pointers around.

As an example, having proofs of various properties of strcat, strcpy, etc. will help less in large programs than having proofs for all Java’s methods on String. In the former, you’ll also have to proof that covers all accesses to your data. In the latter, the JVM guarantees that.

agentultra• 2 years ago

I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps it's writing the automation that is hard right now due to a small overlap in skills.

Writing the proofs is one thing but writing the automation that scales those proofs to a larger system and which makes it easy to extend the system without breaking the proofs constantly is key and requires more "engineering" focused people rather than proof-focused ones.

ReleaseCandidat3• 2 years ago

Some day, I'd love to write proofs instead of tests in some places.

Believe my, you only want to do that if the proof assistent accepts "I leave the details as an exercise to the reader" ;)

tombert7• 2 years ago

I do a lot of work with Isabelle, and when doing proofs, you can use the word "sorry" to basically say "this is true because I said it's true okay".

It's become a running joke in my grad school of "when in doubt, there's always 'proof by sorry'".

I'm not as familiar with a lot of the other proof assistants but I suspect there are similar constructs?

ykonstant6• 2 years ago

For small projects without tight performance or reliability requirements, Lean 4 is fine. It is lacking a lot in basic I/O functions, but you just yank them directly from the C standard library via the FFI and use them in your code. Don't expect to be able to prove anything about your code, though; just treat Lean as a pure functional language like Haskell but with dependent types and eager default evaluation.

nequo2• 2 years ago

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

yodsanklai• 2 years ago

I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either because we're iterating, or because features aren't used anymore. Also, bugs aren't the end of the world most of the time. You don't aim for 100% correctness, but for something that provides value to users and it's better than your competitors. Formal proofs may be useful in some case, but I don't see them outside very niche fields. Even regular static types can be argued against.

rtpg• 2 years ago

Well Coq is used to build a C compiler used in aerospace. At the very least you could write "trricky" stuff in that, and then use the compiled artefacts in your toolkit.

I get the general complaint, though. I wish I could have the syntax-based interactive proof system everywhere.

amw-zero• 2 years ago

Code written in F* is running in Firefox, Linux, Windows, and Azure: https://project-everest.github.io/.

6gvONxR4sf7o2• 2 years ago

Cool! Thanks for the link.

mikhailfranco• 2 years ago

It seems a practical system would do all of the above:

- attempt a proof, could pass or fail, but if it times out, then fall back to...

- property-based test case generation, using logical statements and data generators, shrinking, etc.; many will pass, some will fail, but if some time out ...

- generate simple tests, and edge cases, which may trivially pass, but could be edited by hand to become more useful

If you add a timeout, then exponential runtimes, and even the Halting Problem, always give an answer, even if the answer is to try something simpler.

wyes• 2 years ago

We use F* for some of our crypto for embedded systems software :D

dang• 2 years ago

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)

F* – A Proof-Oriented Programming Language

Related Stories