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

41–50 of 64 posts

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

#41

Post by newpavlov »

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…

>memory safe (without a borrow checker)

This sounds like a very weird statement.

In my opinion, a proper proof-oriented language would inevitably contain a borrow checker variant as a subset of its functionality (assuming the language has notion of pointers/references and focuses on achieving "zero cost abstractions"). Lifetime annotations and shared/exclusive references provide essential information and code use restrictions which enable automatic proof generation.

After all, type and borrow checkers are nothing more than limited forms of automatic proof generation which are practical enough for wide use.

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

#43

Post by hnlmorg »

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?

Neither. It’s always been easy to create a language. What’s been hard is promoting that language.

The things that’s changed is that these days you have a combination of more people using computers plus more convenient forums (like this) for people to promote their new language.

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

#44

Post by mlinksva »

BoingBoomTschak wrote: post #22

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

Looks like it's a predecessor https://www.microsoft.com/en-us/research/project/f7-refineme...

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

#45

Post by agnishom »

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

Somebody managed to write a raytracer with Lean: https://github.com/kmill/lean4-raytracer

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

#46

Post by nextos »

gsbcbdjfncnjd wrote: post #34
nextos wrote: post #21

Earlier quoted context omitted.

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

F* also uses SAT/SMT, specifically Z3.

Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.

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

#47

Post by nextos »

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 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...

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

#48

Post by Taikonerd »

BoingBoomTschak wrote: post #22

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

Is Project Everest still going? The GitHub link says that the repo has been archived...

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

#49

Post by GoblinSlayer »

tdiff wrote: post #37

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.

I wonder why AI doesn't do this verification already. It's a sufficiently simple routine task that doesn't require great precision.

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

#50

Post by mpweiher »

TypingOutBugs wrote: post #12
mpweiher wrote: post #10

Earlier quoted context omitted.

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

F* is a research project thats almost 15 years old! Its not part of the recent wave of languages

Cool!

Though I'd say we've been stuck since about the 80s.

Post reply on HN