[HN Gopher] F*: A proof oriented general purpose programming lan...
___________________________________________________________________
F*: A proof oriented general purpose programming language
Author : akkad33
Score : 133 points
Date : 2024-12-25 13:16 UTC (9 hours ago)
(HTM) web link (fstar-lang.org)
(TXT) w3m dump (fstar-lang.org)
| thunkingdeep wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| As long as you understand that a monad is a monad, you should
| be fine!
| pjmlp wrote:
| Lean also started at MSR, and nowadays is bootstraped, they use
| different approaches.
| jey wrote:
| > 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.
| vb-8448 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| F* is a research project thats almost 15 years old! Its not
| part of the recent wave of languages
| int_19h wrote:
| 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 wrote:
| I wonder if it's a good idea to pick a name that's hard to search
| for...
| amelius wrote:
| ...and that looks like someone is swearing.
| xedrac wrote:
| 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 wrote:
| Foq is hilarious, especially given that just today Coq
| released its website with its new name (Rocq)
| wk_end wrote:
| 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 wrote:
| ".NET"
| fosefx wrote:
| 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.
| seeknotfind wrote:
| 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 wrote:
| 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 wrote:
| 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
| gsbcbdjfncnjd wrote:
| F* also uses SAT/SMT, specifically Z3.
| markusde wrote:
| Do you think you might be able to elaborate a little bit more
| about this?
|
| I was skimming the "Proof-Oriented Programming" book, and it
| seems that the primary way to execute F* programs is by
| extraction or trusted compilation (same as Rocq and Lean, for
| example). Does F* have some special way to work directly with
| realistic source code that these other systems don't?
| seeknotfind wrote:
| F* is a programming language with proof support. Lean/Coq are
| theorem providers that can be used to model and generate
| code. In Coq, there's not a standard way to generate code,
| you might model and create code many different ways. F* seems
| to bring this in as the central goal of the language. So I'm
| discussing this structural difference. F* has an SMT solver,
| but Lean can import an SMT solver. So the goal is the
| important difference here - making theorem proving as
| accessible as possible in a real language. It's a move in the
| right direction, but we want to get to the point standard
| program languages have this support if you need it.
| rajamaka wrote:
| Where would a smooth brained CRUD app web developer who failed
| high school maths perhaps learn more about the point of this?
| seeknotfind wrote:
| The point would be to prove that your database stays
| consistent, a DB upgrade wouldn't break, or that you could
| achieve 100% up time given certain assumptions. An automated
| solver/prover might even be able to tell you where in your
| program breaks this. Without a technology like this, you have
| to carefully read your program, but this is the methodology
| to make the computer deal with that. Unfortunately formal
| verification is mostly used for research, F* is framing
| itself as taking a step to bring that to production
| codebases. Unfortunately I don't know good resources, but as
| researchers adapt this technology, and as we automate a lot
| of the heavy mathematics, you'd never want a programming
| language without this option.
| nickpsecurity wrote:
| I'll add that SPARK Ada allows this now, has commercial tooling
| from Adacore, and was field-prove in years of commercial
| deployments.
|
| https://en.m.wikipedia.org/wiki/SPARK_(programming_language)
|
| It builds on the Why3 platform which also supports Frama-C for
| the C language. IIRC, SPARK can be compiled to C for C-only,
| runtime targets as well.
| madihaa wrote:
| (old discussion) https://news.ycombinator.com/item?id=40377685
| IshKebab wrote:
| I tried to learn F* but honestly it was quite confusing with all
| the different sub-languages and variants.
| kittikitti wrote:
| 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 wrote:
| 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 wrote:
| Isn't it a fundamental limitation of LLMs that we can't?
| rscho wrote:
| Obviously not. It's right in the name, isn't it? LLM =
| limitless model...
| BoingBoomTschak wrote:
| Never used it, but 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) ?
| tdiff wrote:
| 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.
___________________________________________________________________
(page generated 2024-12-25 23:00 UTC)