7 ms·

F*: A proof oriented general purpose programming language

254 points by akkad33 2y ago

thunkingdeep 2y ago
In what situations would one prefer this vs Lean? This seems to compile to native code if desired, so does that mean it’s faster than Lean? Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.
- cess11 2y ago
  Looking at publications on the home pages for both projects it seems F* results in more practical stuff like hardened cryptography and memory allocation libraries, while Lean presents itself as more of an experiment in developing proof assistants.
- markusde 2y ago
  One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis on monadic programming, which I'll admit that I don't understand (but would like to!)
  - ijustlovemath 2y ago
    As long as you understand that a monad is a monad, you should be fine!
- pjmlp 2y ago
  Lean also started at MSR, and nowadays is bootstraped, they use different approaches.
- jey 2y ago
  > F* is oriented toward verified, effectful functional programming for real-world software, while Lean is geared toward interactive theorem proving and formalizing mathematical theories, though both support dependent types and can serve as general-purpose functional languages in principle.
- nextos 2y ago
  Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Semantics was rewritten in Lean [1], but I haven't seen more efforts geared towards software in the Lean community. Dafny, Isabelle, Why3, Coq and F* have been used to verify non-trivial software artifacts. Liquid Haskell, Agda and others are also interesting, but less mature. [1] https://browncs1951x.github.io/static/files/hitchhikersguide.pdf https://browncs1951x.github.io/static/files/hitchhikersguide...
  - TypingOutBugs 2y ago
    Agda and Liquid Haskell are used for Cardano, one of the largest blockchain platforms, alongside other tooling in that space. It’s one of the larger formally verified projects in the wild so I’d argue it’s fairly mature. For example their formal specification of their ledger system: https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmbc2024/OASIcs.FMBC.2024.2/OASIcs.FMBC.2024.2.pdf https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmb...
vb-8448 2y ago
I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?
- gwervc 2y ago
  F* is older than a decade. Also it's a research project, so quite different than the random "memory safe" language iteration of the day.
- mpweiher 2y ago
  I think it's because (a) it's become a lot easier to create languages and (b) we're stuck. I am hoping (a) is straightforward. For (b), I think most of us sense at least intuitively, with different strengths, that our current crop of programming languages are not really good enough. Too low-level, too difficult to get to a more compact and meaningful representation. LLMs have kinda demonstrated the source for this feeling of unease, by generating quite a bit of code from fairly short natural language instructions. The information density of that generated code can't really be all that high, can it now? So we have this issue with expressiveness, but we lack the insight required to make substantial progress. So we bounce around along the well-trodden paths of language design, hoping for progress that refuses to materialize.
  - TypingOutBugs 2y ago
    F* is a research project thats almost 15 years old! Its not part of the recent wave of languages
    - mpweiher 2y ago
      Cool! Though I'd say we've been stuck since about the 80s.
- int_19h 2y ago
  Is there really a proliferation of PLs that hasn't been the case before? I recall many new languages back in 00s as well, it's just that most of them didn't live long enough for people to remember them now.
nottorp 2y ago
I wonder if it's a good idea to pick a name that's hard to search for...
- fosefx 2y ago
  Just like with "golang", "FStar" is the query if choice. But don't think you'll find much, if the documentation is in the same state as it was two years ago.
- amelius 2y ago
  ...and that looks like someone is swearing.
- xedrac 2y ago
  For a language that touts its practicalities, the name isn't a great start. Although F*lang or F***lang (maybe Foq?) seem like reasonable search proxies.
  - markusde 2y ago
    Foq is hilarious, especially given that just today Coq released its website with its new name (Rocq)
- wk_end 2y ago
  Is it really that much harder to search for than "C", "C++", "C#", "F#", "Go", "Rust", "D"...? Googling "Fstar programming language" works fine for me.
  - amelius 2y ago
    ".NET"
  - nottorp 2y ago
    Didn't say those are more inspired. At least Rust is long enough to not get ignored by the search engines. And some of the older ones have being older than the internet as an excuse.
seeknotfind 2y ago
I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write programs and prove parts of them. I believe this is the future of formal languages. If you write something in Rust, it would be great to prove aspects about it. Why not? Well F* is a vision if this future. As proof automation gets better, we will be able to prove many things about our programs, something which is not typically attempted due to difficulty. For instance, imagine proving that a certain path has no allocations, spawns no threads, cannot deadlock, preserves privacy, only modifies a certain subset of global data, is a specific algorithmic complexity, is not subject to timing attacks, maintains the conference of a cache, is memory safe (without a borrow checker). The limit is your imagination and Rice's theorem.
- akkad33 2y ago
  https://dafny.org/ https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe
  - nextos 2y ago
    Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts). It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT. But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1]. [1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
    - gsbcbdjfncnjd 2y ago
      F* also uses SAT/SMT, specifically Z3.
madihaa 2y ago
(old discussion) https://news.ycombinator.com/item?id=40377685 https://news.ycombinator.com/item?id=40377685
IshKebab 2y ago
I tried to learn F* but honestly it was quite confusing with all the different sub-languages and variants.
kittikitti 2y ago
This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM can behave in certain ways within a workflow.
- ijustlovemath 2y ago
  LLMs are fundamentally probabilistic in nature; I think you could prove things about distributions of outputs but nothing like the kind of formal verification you can create with Lean or Rust.
- palata 2y ago
  Isn't it a fundamental limitation of LLMs that we can't?
  - rscho 2y ago
    Obviously not. It's right in the name, isn't it? LLM = limitless model...
- xigoi 2y ago
  An LLM is pretty much a black box. You can’t prove anything meaningful about its output.
- IceDane 2y ago
  You are really comparing apples to oranges here, and to say that trying to apply formal verification to a probabilistic lying machine is silly would be a colossal understatement.
- TypingOutBugs 2y ago
  There’s a few papers in this space but it’s still early days, both using Formal Verification to test outputs of LLMs and using LLMs in formal verification itself Examples of both: https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinating_Jha.pdf https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinati... https://mathai2023.github.io/papers/28.pdf https://mathai2023.github.io/papers/28.pdf
BoingBoomTschak 2y ago
Never used it, but https://github.com/project-everest/mitls-fstar https://github.com/project-everest/mitls-fstar always seems an incredibly cool thing. Huh, apparently there's a successor to F* called F7 (https://github.com/mitls/mitls-flex https://github.com/mitls/mitls-flex) ?
- mlinksva 2y ago
  Looks like it's a predecessor https://www.microsoft.com/en-us/research/project/f7-refinement-types-for-f/ https://www.microsoft.com/en-us/research/project/f7-refineme...
  - BoingBoomTschak 2y ago
    Oh yeah, didn't look at the dates. It's maybe dead, then.
- Taikonerd 2y ago
  Is Project Everest still going? The GitHub link says that the repo has been archived...
tdiff 2y ago
I believe future of programming would vaguely be some mix of intelligent code generation (e.g. LLMs) + formal verification. "LLMs" would be the compiler of the future, something like gcc today, converting "human" language into machine code.
- GoblinSlayer 2y ago
  I wonder why AI doesn't do this verification already. It's a sufficiently simple routine task that doesn't require great precision.
  - IceDane 2y ago
    Formal verification of arbitrary code is a "simple, routine task"?
    - GoblinSlayer 2y ago
      Informal verification.
- shakna 2y ago
  For that, we'd have to have deterministic outputs from the code generator. Which is exactly what the current prospective AI fields don't do. And what the current LLMs cannot.
aranchelk 2y ago
Anyone coming from a Haskell background, there’s some interesting (though possibly dated) info here: https://www.reddit.com/r/haskell/comments/76k1x0/what_do_you_guys_think_of_f_fstar/ https://www.reddit.com/r/haskell/comments/76k1x0/what_do_you...
agnishom 2y ago
I think Lean is another closely related language. It is very famous for its theorem proving capabilities, of course, but it seems that it can also express effectful computations (aka, real world programs). Somebody managed to solve Advent of Code with Lean: https://github.com/anurudhp/aoc2022 https://github.com/anurudhp/aoc2022 Somebody managed to write a raytracer with Lean: https://github.com/kmill/lean4-raytracer https://github.com/kmill/lean4-raytracer
deknos 2y ago
Nice, but as long as at least core and minimal standard library is not really opensource, well maintained and first class citizen on linux, it will not get real distribution. Even C# suffers from that, though it is a nice language. For a programming language to have success it needs to be * opensource * well maintained * first class citizen on win/lin/mac
kodemongos 2y ago
[dead]
spartakos87 2y ago
Where can someone be started with this kind of programming? System verification etc, books? youtube lectures?

254 points by akkad33 2y ago

In what situations would one prefer this vs Lean? This seems to compile to native code if desired, so does that mean it’s faster than Lean? Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.

cess11 2y ago
Looking at publications on the home pages for both projects it seems F* results in more practical stuff like hardened cryptography and memory allocation libraries, while Lean presents itself as more of an experiment in developing proof assistants.
markusde 2y ago
One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis on monadic programming, which I'll admit that I don't understand (but would like to!)
- ijustlovemath 2y ago
  As long as you understand that a monad is a monad, you should be fine!
pjmlp 2y ago
Lean also started at MSR, and nowadays is bootstraped, they use different approaches.
jey 2y ago
> F* is oriented toward verified, effectful functional programming for real-world software, while Lean is geared toward interactive theorem proving and formalizing mathematical theories, though both support dependent types and can serve as general-purpose functional languages in principle.
nextos 2y ago
Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Semantics was rewritten in Lean [1], but I haven't seen more efforts geared towards software in the Lean community. Dafny, Isabelle, Why3, Coq and F* have been used to verify non-trivial software artifacts. Liquid Haskell, Agda and others are also interesting, but less mature. [1] https://browncs1951x.github.io/static/files/hitchhikersguide.pdf https://browncs1951x.github.io/static/files/hitchhikersguide...
- TypingOutBugs 2y ago
  Agda and Liquid Haskell are used for Cardano, one of the largest blockchain platforms, alongside other tooling in that space. It’s one of the larger formally verified projects in the wild so I’d argue it’s fairly mature. For example their formal specification of their ledger system: https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmbc2024/OASIcs.FMBC.2024.2/OASIcs.FMBC.2024.2.pdf https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmb...

vb-8448 2y ago

I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?

gwervc 2y ago
F* is older than a decade. Also it's a research project, so quite different than the random "memory safe" language iteration of the day.
mpweiher 2y ago
I think it's because (a) it's become a lot easier to create languages and (b) we're stuck. I am hoping (a) is straightforward. For (b), I think most of us sense at least intuitively, with different strengths, that our current crop of programming languages are not really good enough. Too low-level, too difficult to get to a more compact and meaningful representation. LLMs have kinda demonstrated the source for this feeling of unease, by generating quite a bit of code from fairly short natural language instructions. The information density of that generated code can't really be all that high, can it now? So we have this issue with expressiveness, but we lack the insight required to make substantial progress. So we bounce around along the well-trodden paths of language design, hoping for progress that refuses to materialize.
- TypingOutBugs 2y ago
  F* is a research project thats almost 15 years old! Its not part of the recent wave of languages
  - mpweiher 2y ago
    Cool! Though I'd say we've been stuck since about the 80s.
int_19h 2y ago
Is there really a proliferation of PLs that hasn't been the case before? I recall many new languages back in 00s as well, it's just that most of them didn't live long enough for people to remember them now.

nottorp 2y ago

I wonder if it's a good idea to pick a name that's hard to search for...

fosefx 2y ago
Just like with "golang", "FStar" is the query if choice. But don't think you'll find much, if the documentation is in the same state as it was two years ago.
amelius 2y ago
...and that looks like someone is swearing.
xedrac 2y ago
For a language that touts its practicalities, the name isn't a great start. Although F*lang or F***lang (maybe Foq?) seem like reasonable search proxies.
- markusde 2y ago
  Foq is hilarious, especially given that just today Coq released its website with its new name (Rocq)
wk_end 2y ago
Is it really that much harder to search for than "C", "C++", "C#", "F#", "Go", "Rust", "D"...? Googling "Fstar programming language" works fine for me.
- amelius 2y ago
  ".NET"
- nottorp 2y ago
  Didn't say those are more inspired. At least Rust is long enough to not get ignored by the search engines. And some of the older ones have being older than the internet as an excuse.

seeknotfind 2y ago

I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write programs and prove parts of them. I believe this is the future of formal languages. If you write something in Rust, it would be great to prove aspects about it. Why not? Well F* is a vision if this future. As proof automation gets better, we will be able to prove many things about our programs, something which is not typically attempted due to difficulty. For instance, imagine proving that a certain path has no allocations, spawns no threads, cannot deadlock, preserves privacy, only modifies a certain subset of global data, is a specific algorithmic complexity, is not subject to timing attacks, maintains the conference of a cache, is memory safe (without a borrow checker). The limit is your imagination and Rice's theorem.

akkad33 2y ago
https://dafny.org/ https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe
- nextos 2y ago
  Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts). It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT. But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1]. [1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
  - gsbcbdjfncnjd 2y ago
    F* also uses SAT/SMT, specifically Z3.

madihaa 2y ago

(old discussion) https://news.ycombinator.com/item?id=40377685 https://news.ycombinator.com/item?id=40377685

IshKebab 2y ago

I tried to learn F* but honestly it was quite confusing with all the different sub-languages and variants.

kittikitti 2y ago

This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM can behave in certain ways within a workflow.

ijustlovemath 2y ago
LLMs are fundamentally probabilistic in nature; I think you could prove things about distributions of outputs but nothing like the kind of formal verification you can create with Lean or Rust.
palata 2y ago
Isn't it a fundamental limitation of LLMs that we can't?
- rscho 2y ago
  Obviously not. It's right in the name, isn't it? LLM = limitless model...
xigoi 2y ago
An LLM is pretty much a black box. You can’t prove anything meaningful about its output.
IceDane 2y ago
You are really comparing apples to oranges here, and to say that trying to apply formal verification to a probabilistic lying machine is silly would be a colossal understatement.
TypingOutBugs 2y ago
There’s a few papers in this space but it’s still early days, both using Formal Verification to test outputs of LLMs and using LLMs in formal verification itself Examples of both: https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinating_Jha.pdf https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinati... https://mathai2023.github.io/papers/28.pdf https://mathai2023.github.io/papers/28.pdf

BoingBoomTschak 2y ago

Never used it, but https://github.com/project-everest/mitls-fstar https://github.com/project-everest/mitls-fstar always seems an incredibly cool thing. Huh, apparently there's a successor to F* called F7 (https://github.com/mitls/mitls-flex https://github.com/mitls/mitls-flex) ?

mlinksva 2y ago
Looks like it's a predecessor https://www.microsoft.com/en-us/research/project/f7-refinement-types-for-f/ https://www.microsoft.com/en-us/research/project/f7-refineme...
- BoingBoomTschak 2y ago
  Oh yeah, didn't look at the dates. It's maybe dead, then.
Taikonerd 2y ago
Is Project Everest still going? The GitHub link says that the repo has been archived...

tdiff 2y ago

I believe future of programming would vaguely be some mix of intelligent code generation (e.g. LLMs) + formal verification. "LLMs" would be the compiler of the future, something like gcc today, converting "human" language into machine code.

GoblinSlayer 2y ago
I wonder why AI doesn't do this verification already. It's a sufficiently simple routine task that doesn't require great precision.
- IceDane 2y ago
  Formal verification of arbitrary code is a "simple, routine task"?
  - GoblinSlayer 2y ago
    Informal verification.
shakna 2y ago
For that, we'd have to have deterministic outputs from the code generator. Which is exactly what the current prospective AI fields don't do. And what the current LLMs cannot.

aranchelk 2y ago

Anyone coming from a Haskell background, there’s some interesting (though possibly dated) info here: https://www.reddit.com/r/haskell/comments/76k1x0/what_do_you_guys_think_of_f_fstar/ https://www.reddit.com/r/haskell/comments/76k1x0/what_do_you...

agnishom 2y ago

I think Lean is another closely related language. It is very famous for its theorem proving capabilities, of course, but it seems that it can also express effectful computations (aka, real world programs). Somebody managed to solve Advent of Code with Lean: https://github.com/anurudhp/aoc2022 https://github.com/anurudhp/aoc2022 Somebody managed to write a raytracer with Lean: https://github.com/kmill/lean4-raytracer https://github.com/kmill/lean4-raytracer

deknos 2y ago

Nice, but as long as at least core and minimal standard library is not really opensource, well maintained and first class citizen on linux, it will not get real distribution. Even C# suffers from that, though it is a nice language. For a programming language to have success it needs to be * opensource * well maintained * first class citizen on win/lin/mac

kodemongos 2y ago

[dead]

spartakos87 2y ago

Where can someone be started with this kind of programming? System verification etc, books? youtube lectures?