[HN Gopher] F* - A Proof-Oriented Programming Language
___________________________________________________________________
F* - A Proof-Oriented Programming Language
Author : montyanderson
Score : 184 points
Date : 2024-05-16 12:47 UTC (10 hours ago)
(HTM) web link (www.fstar-lang.org)
(TXT) w3m dump (www.fstar-lang.org)
| tombert wrote:
| 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.
| jfoutz wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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
|
| 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.
| onhacker wrote:
| 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
| tombert wrote:
| 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 wrote:
| 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.
| daxfohl wrote:
| 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?
| lambdanik wrote:
| 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
| octachron wrote:
| 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.
| lambdanik wrote:
| 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
| tombert wrote:
| 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 wrote:
| Where do you even find orgs that let you program in those fun
| langs?
|
| University jobs?
| tombert wrote:
| 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.
| Nuzzerino wrote:
| I used F# at realtyshares in 2017. Didn't think it was
| particularly great for anything except Payment processing.
| The F# tools were only good with VS IDE on Windows at the
| time. I would probably use it again though, the REPL is
| much better than anything C# has to offer.
|
| The Rider release was a shitshow, lots of bugs that went
| unfixed. Productivity went way down when I had to switch to
| a mac laptop (keep in mind this is 2017 on a Microsoft
| language). Had similar experiences with Rubymine in 2022
| (poor YARD support, lots of bugs in type inference even
| with simple things, bug tickets left open for years, thank
| god for Sorbet-lsp). The tooling is probably better these
| days but I don't trust Jetbrains for anything, they are a
| rent-seeking company.
| neonsunset wrote:
| 2017 was right as the very first releases of .NET Core 1,
| 1.1 and 2.0 were happening.
|
| It's most likely your experience today would be a polar
| opposite to this.
| barrenko wrote:
| There are some trading companies as well, I guess because
| it's ocaml adjacent.
| abeppu wrote:
| 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?
| jfoutz wrote:
| 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".
| abeppu wrote:
| 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
| octachron wrote:
| 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 .
| eggy wrote:
| 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 wrote:
| 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 wrote:
| 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.
| debugnik wrote:
| > 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.
| eggy wrote:
| 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.
| pelagicAustral wrote:
| 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
| seanw444 wrote:
| 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 wrote:
| Agree, and there are other projects with fun names like
| https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation)
| pelagicAustral wrote:
| "Coon - new tool for building Erlang packages, dependency
| management and deploying Erlang services" [0] comes to
| mind. Highly recommendable thread to read.
|
| 0: https://erlang.org/pipermail/erlang-
| questions/2018-February/...
| wk_end wrote:
| It's odd how this is deemed acceptable - Wikipedia explains
| that the joke is in reference to its "brutal" optimization,
| which I'm sure eastern Europeans find hilarious (they
| might, they're known for their grim sense of humour) - but
| no one would seriously consider naming, say, their fork of
| the GNU assembler "Hitler".
| seanw444 wrote:
| Stalin never earned the same perception as Hitler,
| probably because he won and Hitler didn't. History is
| written by the victors. There's a reason the cliche move
| in politics is to call your opponent "literally Hitler"
| and not "literally Stalin". That said, I doubt any tool
| named "Stalin" would gain any major traction. Adopting
| such a tool would be a huge liability for a company.
| debugnik wrote:
| 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.
| kgeist wrote:
| -nik is a suffix which exists in all Slavic languages,
| including Ukrainian. Nothing specifically Russian about it.
| andrewflnr wrote:
| And even if it was, poking gentle fun at a Russian suffix
| would not be an endorsement of the invasion.
| debugnik wrote:
| I, personally, am aware, but I'm not so sure everyone who
| will read my username knows that, and there's enough war-
| related shilling around (and suspicion thereof) that the
| pun simply isn't worth it.
| chuckadams wrote:
| Yeesh, avoiding obvious Russian-isms is one thing, but a
| common suffix? I say _Nyet!_ Anyone triggered by that isn't
| worth accommodating.
| wisemang wrote:
| 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.
| unstruktured wrote:
| F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/) would be the
| ultimate experience. I was born too early!
| wk_end wrote:
| 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.
| unstruktured wrote:
| 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 wrote:
| I'm curious how similar F* is to Lean Prover (which I've dabbled
| in).
| slushy-chivalry wrote:
| and both are backed by msft?
| bmitc wrote:
| 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 wrote:
| 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.
| lambdanik wrote:
| Not just marketing ...
|
| About the name: https://fstar-
| lang.org/tutorial/book/intro.html#a-bit-of-f-h...
| mkehrt wrote:
| 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 wrote:
| It makes me miss my time spent tinkering with Idris :)
| User23 wrote:
| 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.
| 082349872349872 wrote:
| > _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?
| chuckadams wrote:
| 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")
| 6gvONxR4sf7o wrote:
| 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.
| bluGill wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| ReleaseCandidat wrote:
| > 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" ;)
| tombert wrote:
| 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?
| nextaccountic wrote:
| > 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".
|
| I always thought that unsafe { .. } blocks in Rust should
| be called trustme { .. }
|
| But sorry { .. } is even better!
| tombert wrote:
| Yeah, it's pretty funny to see the first draft of
| anything I'm trying to prove; it'll be polluted with
| sorry's everywhere; it comes off as the most apologetic,
| completely un-confident bit of math you can think of.
|
| The worst part is when you forget to remove a sorry (or
| three) because of a linked file you didn't check, and you
| submit stuff to other people on the team thinking you
| discovered something pretty cool, only to find out that
| you didn't actually prove anything.
| ReleaseCandidat wrote:
| My favorite is accursedUnutterablePerformIO https://hacka
| ge.haskell.org/package/bytestring-0.12.1.0/docs...
| This "function" has a superficial similarity to
| unsafePerformIO but it is in fact a malevolent agent of
| chaos. It unpicks the seams of reality (and the IO monad)
| so that the normal rules no longer apply. It lulls you
| into thinking it is reasonable, but when you are not
| looking it stabs you in the back and aliases all of your
| mutable buffers. The carcass of many a seasoned Haskell
| programmer lie strewn at its feet.
| ReleaseCandidat wrote:
| Coq has "admitted" (or "admit"), but sorry is of course way
| better :). Lean also has "admit".
| dunham wrote:
| Lean has `sorry` and Idris has `believe_me`. Recalling my
| math education, I would think the appropriate keyword would
| be `clearly`.
| ykonstant wrote:
| 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.
| nequo wrote:
| 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?
| ykonstant wrote:
| By far the main impediment is that the current community
| does not care about this use-case. Lean's proof system
| works mainly by using its metaprogramming aspects to write
| macro-type objects called tactics; they perform
| transformations on the goals of your proof to simplify or
| dispatch them.
|
| [Note that this meta-programming is very powerful, but also
| extremely hard to use from what I have managed to see; do
| not expect LISP style ergonomics here. It doesn't help that
| the meta-programming book shows some trivial examples of
| macro rules and then delves deep into proof tactics for the
| next 2 chapters, leaving the reader who wants general code
| transformations stranded].
|
| In order to use Lean for proving properties for serious
| amounts of code, you need to write an entire tactics
| library similar to mathlib (but for code). Nobody has done
| this. Maybe it is reasonably hard, or maybe unreasonably
| hard; the point is, there is no serious collaborative
| effort that I know of.
| nequo wrote:
| Do you get the sense that this would be easier with Coq
| due to the availability of suitable tactics? What makes
| you pick Lean instead of Coq for your projects?
| ykonstant wrote:
| Probably, from what people are telling me. But Coq is not
| a general purpose language, it is a dedicated theorem
| prover. I don't use Lean as a theorem prover for code
| (only for mathematics) and I myself don't do any code
| formalization unless someone offers to pay me.
|
| The reason I code in Lean is because I find it fun, and I
| think it is a very nice general purpose language; for
| instance, I like Lean much better than Haskell. If Lean
| ever gets the libraries Haskell has, I will be really
| excited.
| yodsanklai wrote:
| 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 wrote:
| 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.
| wyes wrote:
| We use F* for some of our crypto for embedded systems software :D
___________________________________________________________________
(page generated 2024-05-16 23:00 UTC)