Live data from Hacker News

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

fstar-lang.org

41–50 of 107 posts

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

#41

Earlier quoted context omitted.

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?

There's a difference, yes. How big it is isn't really relevant question cause its simply an unnecessary tax on visitors.

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

#43
post #12

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.

Use case. Not “user case”.

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

#44
post #26

Earlier quoted context omitted.

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

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.

What is code edition?

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

#45

Earlier quoted context omitted.

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…

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

> 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

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

#46

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

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

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

#47
post #7

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

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.

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.

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

#48

Earlier quoted context omitted.

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

> 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

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

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

#49
post #26

Earlier quoted context omitted.

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.

What is code edition?

> What is code edition?

I think rixed means "code editing" (I guess that rixed is simply not a native (L1) or excellent L2 English speaker).

Post reply on HN