Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

fstar-lang.org

Post reply on HN
Print view View original

11–20 of 107 posts

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

#11

Post by cyanregiment »

aleph_minus_one wrote: post #8
munchler wrote: post #6

Earlier quoted context omitted.

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 (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…

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!

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

#12

Post by rixed »

cyanregiment wrote: post #3

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

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.

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

#13

Post by cyanregiment »

rainyq wrote: post #4
cyanregiment wrote: post #3

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

just click the screenshot

Takes you to an empty editor with still no code examples

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

#14

Post by [deleted] »

qzzi wrote: post #5
cyanregiment wrote: post #3

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

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

[deleted]

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

#16

Post by sroerick »

rixed wrote: post #12
cyanregiment wrote: post #3

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

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.

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

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

#19

Post by zlsa »

sroerick wrote: post #16
rixed wrote: post #12

Earlier quoted context omitted.

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.

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

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