Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

F*: A proof oriented general purpose programming language

fstar-lang.org

Post reply on HN
Print view View original

21–30 of 64 posts

Re: F*: A proof oriented general purpose programming language

#21

Post by nextos »

akkad33 wrote: post #8
seeknotfind wrote: post #7

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 pr…

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

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

Re: F*: A proof oriented general purpose programming language

#23

Post by ijustlovemath »

kittikitti wrote: post #20

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.

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.

Re: F*: A proof oriented general purpose programming language

#24

Post by ijustlovemath »

markusde wrote: post #9
thunkingdeep wrote: post #2

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.

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!)

As long as you understand that a monad is a monad, you should be fine!

Re: F*: A proof oriented general purpose programming language

#25

Post by [deleted] »

akkad33 wrote: post #8
seeknotfind wrote: post #7

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 pr…

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

[deleted]

Re: F*: A proof oriented general purpose programming language

#26

Post by pjmlp »

thunkingdeep wrote: post #2

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.

Lean also started at MSR, and nowadays is bootstraped, they use different approaches.

Re: F*: A proof oriented general purpose programming language

#27

Post by palata »

kittikitti wrote: post #20

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.

Isn't it a fundamental limitation of LLMs that we can't?

Re: F*: A proof oriented general purpose programming language

#28

Post by rajamaka »

seeknotfind wrote: post #7

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 pr…

Where would a smooth brained CRUD app web developer who failed high school maths perhaps learn more about the point of this?

Re: F*: A proof oriented general purpose programming language

#29

Post by int_19h »

vb-8448 wrote: post #3

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?

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.

Re: F*: A proof oriented general purpose programming language

#30

Post by seeknotfind »

markusde wrote: post #11
seeknotfind wrote: post #7

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 pr…

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?

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.
Post reply on HN