Hacker News

by Ryan Harman

F*: A general-purpose proof-oriented programming language (fstar-lang.org)

118 points by ducktective 8 hours ago

cyanregiment 6 hours ago

Clicked like 5 pages and never found 1 code example.

Idk why languages don't have their syntax in a sandbox front-and-center on the home page.

It's like a video game site with zero screenshots or videos (also rampant).

New programming languages I want 2 things:

1. What does the syntax look like

2. Why would I use this language

Talk about the proof logic, show the syntax, thank you

Verdex 6 hours ago

To borrow your video game analogy. F* is the dwarf fortress of programming languages. Screenshots are only going to confuse anyone who isn't ready to take a significant mental journey.

redrobein 35 minutes ago

This is needless fearmongering. F* looks a lot like F# code with semantics you should be familiar with if you've worked with other proof oriented languages. The website design is dated is all. The book gives exactly what the OP wants in the introductory chapter.

rixed 5 hours ago

I'm the opposite: when landing in a programming language site I want to know the user case the authors had in mind, the memory model, the type system, the compilation targets, the data layout, the control structures, and only at the end just check that the syntax is not indentation based.

sroerick 5 hours ago

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

Georgelemental 4 minutes ago

rixed 4 hours ago

mcluck 2 hours ago

dunham 3 hours ago

zlsa 5 hours ago

giancarlostoro 4 hours ago

NuclearPM an hour ago

Use case. Not “user case”.

kasumispencer2 4 hours ago

> Clicked like 5 pages and never found 1 code example.

But I clicked one (1) link to the online book and found a thousand?

giancarlostoro 4 hours ago

Should be on the home page of any programming language site.

kasumispencer2 4 hours ago

munchler 6 hours ago

https://fstar-lang.org/tutorial/

_flux 5 hours ago

I guess it's a bit popular right now

    * Error 17 at Welcome.fst(24,0-28,30):
      - Could not start SMT solver process.
      - Command: ‘/home/site/wwwroot/fstar/bin/z3’
      - Exception:
          Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
    
    1 error was reported (see above)

aleph_minus_one 6 hours ago

> https://fstar-lang.org/tutorial/

FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

> https://fstar-lang.org/index.html#learn (1)

and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

In the section of (1) also the PDF version is linked:

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

cyanregiment 5 hours ago

rainyq 6 hours ago

just click the screenshot

cyanregiment 5 hours ago

Takes you to an empty editor with still no code examples

summarity 36 minutes ago

What? There’s literally a completely interactive book linked right from the home page.

remywang 4 hours ago

That’s because syntax is the least interesting part of F*.

thomastjeffery 4 hours ago

Then why are we all so interested?

Examples provide more than syntax. It's the semantics that we care about most.

aleph_minus_one 4 hours ago

voodooEntity 3 hours ago

Thank you ! I just had the absolute same experience and was about to write a similar comment - take my upvote instead !

qzzi 6 hours ago

I clicked on 2 links on the main page in the Learn F* section...

LelouBil 10 minutes ago

[delayed]

LelouBil 22 minutes ago

I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.

Is this used in the industry ? And for what kind of software ?

LelouBil 16 minutes ago

I found these links in the F* book

https://www.microsoft.com/en-us/research/blog/everparse-hard...

https://lwn.net/Articles/770750/

https://project-everest.github.io/

pvsnp 6 hours ago

I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.

rixed 4 hours ago

What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?

boutell an hour ago

I guess responsive stylesheets can't be implemented without side effects...

3lambda 5 hours ago

Would this language be useful for implementing compilers and formally proving things about them?

physPop 2 hours ago

yes thats the main reason, agda , coq similar ideas

IshKebab 5 hours ago

F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out.

Does it get basic stuff like subtraction and u8 right, unlike Lean?