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

81–90 of 107 posts

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

#81

Post by floxy »

dunham wrote: post #38
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 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…

>a rename might affect indentation

I think I need to see an example.

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

#82

Post by throw234234234 »

mcluck wrote: post #39
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?

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

I suspect this is a "what you are used to" and have trained yourself to look out for over many years of code reading.

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

#83

Post by _thejanus_ »

_doctor_love wrote: post #63

Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?

Yes, I’ve used the EverParse lib, as well as low* extensively! I found a really nice use case, low* makes writing bare metal protocol parsers incredibly easy and compositional at no obvious cost to performance. It’s a real breath of fresh air compared to writing one giant horrible whole loop, but it basically optimises down to the same assembly.

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

#84

Post by _thejanus_ »

dnautics wrote: post #61
3lambda wrote: post #15

Would this language be useful for implementing compilers and formally proving things about them?

personally i think you should just have a separate proof language that doesn't also try to be a programming language and build a bridge between them (ideally as a compilation target). anyways im working on this with my spare opus tokens.

What do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this.

Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly

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

#86

Post by _thejanus_ »

3lambda wrote: post #15

Would this language be useful for implementing compilers and formally proving things about them?

I think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive enough that your source language can be pretty wild with your denotational semantics. Grain of salt though, because I haven’t tried this concept in anger at all

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

#88

Post by bmitc »

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.

You'll be disappointed in F* then.

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

#89

Post by bmitc »

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

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

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

#90

Post by bmitc »

vivzkestrel wrote: post #87

- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust

That language is basically F#, except for perhaps the performance claims. But F# is definitely not a slow language.
Post reply on HN