▲ _flux 6 hours ago | parent | next [-]

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 | parent | prev [-]

> 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 6 hours ago | parent [-]

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!

▲

aleph_minus_one 4 hours ago | parent [-]

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

Often the reason is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested

> "HTTP server", "hello world", "todo list app"

in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.

▲

cyanregiment an hour ago | parent [-]

> just look at which web framework

See, by listing those, you can tell what it is.

I imagine the quick project showcase would be different for Swift or for Rust.

Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

Like what kinds of things i can even think of writing with it - an implementation example

▲

aleph_minus_one an hour ago | parent [-]

> I imagine the quick project showcase would be different for Swift or for Rust.

> Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

I suggest simply having a look at the table of contents of

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

This in my opinion gives you a first rough idea for what kind of problems people are using F*.

Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

This is exactly the reason why I wrote further above:

> Often the reason [why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app"] is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

	▲	cyanregiment 43 minutes ago \| parent [-]
		> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...]. Ok, what kinds of problems are they? And ideally - what does a simple solution look like in F-star? Set me on the path to installing the thing (ideally above the fold)