5 ms·

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 vid

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

rainyq 2mo ago
just click the screenshot
- cyanregiment 2mo ago
  Takes you to an empty editor with still no code examples
qzzi 2mo ago
I clicked on 2 links on the main page in the Learn F* section...
- deleted 2mo ago
  [deleted]
munchler 2mo ago
https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
- aleph_minus_one 2mo ago
  > https://fstar-lang.org/tutorial/ 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 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-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i...
  - cyanregiment 2mo 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!
    - aleph_minus_one 2mo ago
      > 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 2mo ago
        > 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 2mo ago
        > 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-in-fstar.pdf 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.
- _flux 2mo 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)
Verdex 2mo 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 2mo 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.
  - Verdex 2mo ago
    Fearmonger? Me? Well I never. Also > if you've worked with other proof oriented languages. That's doing a lot of heavy lifting.
    - _doctor_love 2mo ago
      Fearmonger is a little heavy handed but the comparison to Dwarf Fortress is probably too strong. I don't find F* syntax anymore intimidating than Haskell, Scala, Mercury, Prolog, etc. aka the hard languages. I love Ruby and I didn't find it intuitive when I first began learning it (specifically, the block/lambda passing mechanism).
      - Verdex 2mo ago
        Meanwhile I'm sure there's people out there baffled that anyone finds dwarf fortress challenging to get into. I'm old enough that I've had the pleasure of handholding software engineers through their first anonymous function usage. Effect system, refinement types, totality checker? The best I get is blank stares before they go back to C# and JavaScript. These days I'm just glad they tolerate linq expressions and typescript. It matters where you're standing for what feels incomprehensible. But then again, you can say the same thing about dwarf fortress.
rixed 2mo 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 2mo ago
  So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?
  - zlsa 2mo ago
    I think this falls under "[wanting] to know the user case the authors had in mind"
    - BretonForearm 2mo ago
      There is no "user case", it's called use case.
      - aleph_minus_one 2mo ago
        > There is no "user case", it's called use case. Perhaps English is not a native language for zlsa?
  - rixed 2mo 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.
    - NuclearPM 2mo ago
      What is code edition?
kasumispencer2 2mo 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?
- deleted 2mo ago
  [deleted]
- giancarlostoro 2mo ago
  Should be on the home page of any programming language site.
  - kasumispencer2 2mo 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?
    - broken-kebab 2mo ago
      There's a difference, yes. How big it is isn't really relevant question cause its simply an unnecessary tax on visitors.
remywang 2mo ago
That’s because syntax is the least interesting part of F*.
- thomastjeffery 2mo 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 2mo 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-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i... > https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
    - derdi 2mo ago
      The OP doesn't want encompassing, they want the following example from the tutorial on the front page: type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1) let rec append #a #n #m (v1:vec a n) (v2:vec a m) : vec a (n + m) = match v1 with | Nil -> v2 | Cons hd tl -> Cons hd (append tl v2) This is a completely reasonable thing to want and expect. Edit: For comparison, Rocq https://rocq-prover.org/ https://rocq-prover.org/ and Lean https://lean-lang.org/ https://lean-lang.org/ both manage to do this.
      - rybosome 2mo ago
        I'm not the OP, but this is exactly my interpretation, and my gripe with the homepage as well in lacking this concise yet powerful example. You can tell a lot about a programming language by looking at the right snippet.
voodooEntity 2mo ago
Thank you ! I just had the absolute same experience and was about to write a similar comment - take my upvote instead !
summarity 2mo ago
What? There’s literally a completely interactive book linked right from the home page.
bmitc 2mo ago
Two clicks take you to the tutorial: https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/

rainyq 2mo ago

just click the screenshot

cyanregiment 2mo ago
Takes you to an empty editor with still no code examples

qzzi 2mo ago

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

deleted 2mo ago
[deleted]

munchler 2mo ago

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

aleph_minus_one 2mo ago
> https://fstar-lang.org/tutorial/ 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 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-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i...
- cyanregiment 2mo 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!
  - aleph_minus_one 2mo ago
    > 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 2mo ago
      > 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 2mo ago
        > 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-in-fstar.pdf 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.
_flux 2mo 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)

Verdex 2mo 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 2mo 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.
- Verdex 2mo ago
  Fearmonger? Me? Well I never. Also > if you've worked with other proof oriented languages. That's doing a lot of heavy lifting.
  - _doctor_love 2mo ago
    Fearmonger is a little heavy handed but the comparison to Dwarf Fortress is probably too strong. I don't find F* syntax anymore intimidating than Haskell, Scala, Mercury, Prolog, etc. aka the hard languages. I love Ruby and I didn't find it intuitive when I first began learning it (specifically, the block/lambda passing mechanism).
    - Verdex 2mo ago
      Meanwhile I'm sure there's people out there baffled that anyone finds dwarf fortress challenging to get into. I'm old enough that I've had the pleasure of handholding software engineers through their first anonymous function usage. Effect system, refinement types, totality checker? The best I get is blank stares before they go back to C# and JavaScript. These days I'm just glad they tolerate linq expressions and typescript. It matters where you're standing for what feels incomprehensible. But then again, you can say the same thing about dwarf fortress.

rixed 2mo 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 2mo ago
So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?
- zlsa 2mo ago
  I think this falls under "[wanting] to know the user case the authors had in mind"
  - BretonForearm 2mo ago
    There is no "user case", it's called use case.
    - aleph_minus_one 2mo ago
      > There is no "user case", it's called use case. Perhaps English is not a native language for zlsa?
- rixed 2mo 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.
  - NuclearPM 2mo ago
    What is code edition?

kasumispencer2 2mo 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?

deleted 2mo ago
[deleted]
giancarlostoro 2mo ago
Should be on the home page of any programming language site.
- kasumispencer2 2mo 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?
  - broken-kebab 2mo ago
    There's a difference, yes. How big it is isn't really relevant question cause its simply an unnecessary tax on visitors.

remywang 2mo ago

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

thomastjeffery 2mo 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 2mo 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-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i... > https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
  - derdi 2mo ago
    The OP doesn't want encompassing, they want the following example from the tutorial on the front page: type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1) let rec append #a #n #m (v1:vec a n) (v2:vec a m) : vec a (n + m) = match v1 with | Nil -> v2 | Cons hd tl -> Cons hd (append tl v2) This is a completely reasonable thing to want and expect. Edit: For comparison, Rocq https://rocq-prover.org/ https://rocq-prover.org/ and Lean https://lean-lang.org/ https://lean-lang.org/ both manage to do this.
    - rybosome 2mo ago
      I'm not the OP, but this is exactly my interpretation, and my gripe with the homepage as well in lacking this concise yet powerful example. You can tell a lot about a programming language by looking at the right snippet.

voodooEntity 2mo ago

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

summarity 2mo ago

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

bmitc 2mo ago

Two clicks take you to the tutorial: https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/