11 ms·

F* – A Proof-Oriented Programming Language

236 points by montyanderson 2y ago

tombert 2y 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.
- jfoutz 2y 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.
  - ykonstant 2y 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).
    - eggy 2y ago
      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 2y ago
        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 https://news.ycombinator.com/item?id=31775216 Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language) 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.
        eggy 2y ago
        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.
- onhacker 2y 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
  - tombert 2y 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 2y 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.
    - 2y ago
- daxfohl 2y 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?
  - octachron 2y ago
    The Everest project did publish a proved TLS implementation: https://mitls.org https://mitls.org. And at least the EverCrypt* cryptographic primitives has been used outside of academia.
  - lambdanik 2y 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/ 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-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/ https://www.microsoft.com/en-us/research/blog/everparse-hard... * Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star
    - daxfohl 2y ago
      So _would_ it possibly be useful for business apps? Or is that still a long way off?
- lambdanik 2y ago
  Have you seen https://github.com/FStarLang/fstar-vscode-assistant 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 https://github.com/FStarLang/fstar-mode.el
  - tombert 2y 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 2y ago
  Where do you even find orgs that let you program in those fun langs? University jobs?
  - tombert 2y 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.
    - celdon25 2y ago
      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 2y ago
        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.
  - norealmet 2y ago
    [dead]
  - barrenko 2y ago
    There are some trading companies as well, I guess because it's ocaml adjacent.
  - happypumpkin 2y ago
abeppu 2y 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?
- jfoutz 2y 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".
  - abeppu 2y 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
- octachron 2y 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 .
eggy 2y 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 2y 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 2y ago
    Fairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html 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 2y 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.
  - eggy 2y 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.
pelagicAustral 2y 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 https://github.com/FStarLang/FStar/pull/2489
- seanw444 2y 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 2y ago
    Agree, and there are other projects with fun names like https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation) https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation)
    - pelagicAustral 2y ago
      "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/thread.html#94769 https://erlang.org/pipermail/erlang-questions/2018-February/...
    - wk_end 2y ago
      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".
unstruktured 2y ago
F* + 1ml (https://people.mpi-sws.org/~rossberg/1ml/ https://people.mpi-sws.org/~rossberg/1ml/) would be the ultimate experience. I was born too early!
- wk_end 2y 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.
  - unstruktured 2y 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 2y ago
I'm curious how similar F* is to Lean Prover (which I've dabbled in).
- slushy-chivalry 2y ago
  and both are backed by msft?
bmitc 2y 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 2y 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.
  - lambdanik 2y ago
    Not just marketing ... About the name: https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-history https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-h...
  - mkehrt 2y 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 2y ago
It makes me miss my time spent tinkering with Idris :)
User23 2y 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 https://link.springer.com/book/10.1007/978-1-4612-3228-5 [2] https://dl.acm.org/doi/10.1145/2499370.2491978 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 2y 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?
  - chuckadams 2y 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”)
  - vinnyvichy 2y 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-judgment-a-review/ https://quillette.com/2022/04/05/noise-a-flaw-in-human-judgm... https://www.newscientist.com/article/2431131-buildings-that-include-weak-points-on-purpose-withstand-more-damage/ https://www.newscientist.com/article/2431131-buildings-that-...
6gvONxR4sf7o 2y 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.
- bluGill 2y 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 2y 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 2y 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 2y 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.
wyes 2y ago
We use F* for some of our crypto for embedded systems software :D
dang 2y ago
Related. Others? The F* Programming Language - https://news.ycombinator.com/item?id=31517176 https://news.ycombinator.com/item?id=31517176 - May 2022 (6 comments) Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=25629058 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 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 https://news.ycombinator.com/item?id=12753788 - Oct 2016 (2 comments) Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=10949288 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 https://news.ycombinator.com/item?id=2663240 - June 2011 (9 comments)

236 points by montyanderson 2y 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.

jfoutz 2y 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.
- ykonstant 2y 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).
  - eggy 2y ago
    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 2y ago
      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 https://news.ycombinator.com/item?id=31775216 Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language) 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.
      - eggy 2y ago
        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.
onhacker 2y 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
- tombert 2y 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 2y 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.
  - 2y ago
daxfohl 2y 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?
- octachron 2y ago
  The Everest project did publish a proved TLS implementation: https://mitls.org https://mitls.org. And at least the EverCrypt* cryptographic primitives has been used outside of academia.
- lambdanik 2y 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/ 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-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/ https://www.microsoft.com/en-us/research/blog/everparse-hard... * Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star
  - daxfohl 2y ago
    So _would_ it possibly be useful for business apps? Or is that still a long way off?
lambdanik 2y ago
Have you seen https://github.com/FStarLang/fstar-vscode-assistant 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 https://github.com/FStarLang/fstar-mode.el
- tombert 2y 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 2y ago
Where do you even find orgs that let you program in those fun langs? University jobs?
- tombert 2y 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.
  - celdon25 2y ago
    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 2y ago
      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.
- norealmet 2y ago
  [dead]
- barrenko 2y ago
  There are some trading companies as well, I guess because it's ocaml adjacent.
- happypumpkin 2y ago

abeppu 2y 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?

jfoutz 2y 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".
- abeppu 2y 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
octachron 2y 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 .

eggy 2y 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 2y 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 2y ago
  Fairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html 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 2y 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.
- eggy 2y 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.

pelagicAustral 2y 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 https://github.com/FStarLang/FStar/pull/2489

seanw444 2y 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 2y ago
  Agree, and there are other projects with fun names like https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation) https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation)
  - pelagicAustral 2y ago
    "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/thread.html#94769 https://erlang.org/pipermail/erlang-questions/2018-February/...
  - wk_end 2y ago
    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".

unstruktured 2y ago

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

wk_end 2y 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.
- unstruktured 2y 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 2y ago

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

slushy-chivalry 2y ago
and both are backed by msft?

bmitc 2y 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 2y 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.
- lambdanik 2y ago
  Not just marketing ... About the name: https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-history https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-h...
- mkehrt 2y 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 2y ago

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

User23 2y 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 https://link.springer.com/book/10.1007/978-1-4612-3228-5 [2] https://dl.acm.org/doi/10.1145/2499370.2491978 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 2y 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?
- chuckadams 2y 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”)
- vinnyvichy 2y 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-judgment-a-review/ https://quillette.com/2022/04/05/noise-a-flaw-in-human-judgm... https://www.newscientist.com/article/2431131-buildings-that-include-weak-points-on-purpose-withstand-more-damage/ https://www.newscientist.com/article/2431131-buildings-that-...

6gvONxR4sf7o 2y 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.

bluGill 2y 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 2y 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 2y 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 2y 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.

wyes 2y ago

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

dang 2y ago

Related. Others? The F* Programming Language - https://news.ycombinator.com/item?id=31517176 https://news.ycombinator.com/item?id=31517176 - May 2022 (6 comments) Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=25629058 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 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 https://news.ycombinator.com/item?id=12753788 - Oct 2016 (2 comments) Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=10949288 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 https://news.ycombinator.com/item?id=2663240 - June 2011 (9 comments)