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

11–20 of 64 posts

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

#11

Post by markusde »

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?

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

#12

Post by TypingOutBugs »

mpweiher wrote: post #10
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?

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

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

#17

Post by markusde »

xedrac wrote: post #16
nottorp wrote: post #5

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

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.

Foq is hilarious, especially given that just today Coq released its website with its new name (Rocq)

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

#19

Post by amelius »

wk_end wrote: post #18
nottorp wrote: post #5

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

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.

".NET"
Post reply on HN