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

dducktective about 6 hours ago 31 commentsRead Article on fstar-lang.org

ES version is available. Content is displayed in original English for accuracy.

⚡ Community Insights

Discussion Sentiment

57% Positive

Analyzed from 734 words in the discussion.

Discussion (31 Comments)Read Original on HackerNews

cyanregiment•about 4 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

kasumispencer2•about 2 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•about 1 hour ago

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

kasumispencer2•about 1 hour ago

Is there actually any difference when it's just one (1) link away? Are most of us seriously this busy that we cannot spend even half a minute on this?

rixed•about 3 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•about 3 hours ago

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

dunham•37 minutes ago

I don't mind indentation based languages. I used to hate them, but they've grown on me after using python, Haskell, Idris, Agda, etc. And I ended up making my own language indentation based (it is similar to Idris).

That said, it is hard-mode:

- You'll have to figure out how to parse it.

- If you want editor support, it's a pain to get tree-sitter to handle it.

- You may not be able to pull off editor operations like "rename" without implementing a pretty printer (a rename might affect indentation).

I think it is helpful for crude error recovery. On parse error, my language will simply skip to the next column 0 token and parse another declaration.

I did not do this (hindsight), but I would recommend arranging the grammar so you only get indented blocks in cases where the previous line ends in a keyword that introduces it. I think python has a trailing `:` every time indentation is introduced, and Elm does this too - in statements like `let` you need a newline after the `let` to get the multi-declaration version. (This addresses the rename issue.)

rixed•about 2 hours ago

No indeed I'm not a fan. I find it brittle and arbitrary for data values especially; that also makes automatic code generation and edition harder, for no good reason. But that's not an important consideration either way.

zlsa•about 2 hours ago

I think this falls under "[wanting] to know the user case the authors had in mind"

giancarlostoro•about 1 hour ago

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

Verdex•about 3 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.

munchler•about 3 hours ago

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

_flux•about 3 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•about 3 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•about 3 hours ago

I still don't see any code examples!

But I do see the editor to try it.

I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance

Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!

voodooEntity•about 1 hour ago

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

rainyq•about 3 hours ago

just click the screenshot

cyanregiment•about 3 hours ago

Takes you to an empty editor with still no code examples

remywang•about 2 hours ago

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

thomastjeffery•about 2 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•about 2 hours ago

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

... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*":

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

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

qzzi•about 3 hours ago

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

pvsnp•about 4 hours ago

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

rixed•about 2 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?

3lambda•about 3 hours ago

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

IshKebab•about 2 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?