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

31–40 of 107 posts

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

#32

Post by giancarlostoro »

kasumispencer2 wrote: post #21
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

> Clicked like 5 pages and never found 1 code example. But I clicked one (1) link to the online book and found a thousand?

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

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

#33

Post by giancarlostoro »

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 love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

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

#34

Post by koolala »

giancarlostoro wrote: post #33
sroerick wrote: post #16

Earlier quoted context omitted.

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

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.

Isn't it easy to just auto format it?

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

#35

Post by kasumispencer2 »

giancarlostoro wrote: post #32
kasumispencer2 wrote: post #21

Earlier quoted context omitted.

> Clicked like 5 pages and never found 1 code example. But I clicked one (1) link to the online book and found a thousand?

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

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?

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

#37

Post by voodooEntity »

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

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

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

#38

Post by dunham »

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

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

#39

Post by mcluck »

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?

For what it's worth, I love the semantics of many indentation based languages (F# for example) but really dislike editing them. Visually scanning is much easier with braces (imo) and it's much easier to navigate braced languages when using a vim-like editor
Post reply on HN