Rendered at 05:31:26 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
cyanregiment 15 hours ago [-]
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
rixed 14 hours 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 14 hours ago [-]
So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?
Georgelemental 9 hours ago [-]
Indentation based is a pain when copy-pasting between contexts with different indentation levels, as you have to fix it up manually, which is error-prone. In languages without it, you can just auto-format. (And even in an editor that doesn't support that, having a second indicator makes it less error-prone to fix manually)
floxy 2 hours ago [-]
>copy-pasting
Underappreciated benefit of side benefit of indentation based languages: no copy-pasta.
teiferer 8 hours ago [-]
> have to fix it up manually
Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).
jcgl 8 hours ago [-]
But that doesn't work if the indentation carries semantic meaning; you can't change the indentation without changing the meaning. Maybe you can correct syntactically-incorrect spacing (e.g. change 3 spaces to 4 spaces), but not much beyond that.
rixed 13 hours 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 10 hours ago [-]
What is code edition?
aleph_minus_one 10 hours ago [-]
> 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).
mcluck 11 hours ago [-]
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
teiferer 8 hours ago [-]
For somebody unable to empathize with the "braces are easier to scan" part, could yiu explain why?
I find it easy to see if things are on the same indentation. I find it much harder to visually scan for opening and closing braces unless syntax highliting makes them scream at me or they are accompanied by ...indentation.
throw234234234 2 hours ago [-]
I suspect this is a "what you are used to" and have trained yourself to look out for over many years of code reading.
dunham 12 hours ago [-]
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.)
floxy 2 hours ago [-]
>a rename might affect indentation
I think I need to see an example.
zlsa 14 hours ago [-]
I think this falls under "[wanting] to know the user case the authors had in mind"
BretonForearm 13 hours ago [-]
There is no "user case", it's called use case.
aleph_minus_one 13 hours ago [-]
> There is no "user case", it's called use case.
Perhaps English is not a native language for zlsa?
dataflow 5 hours ago [-]
Honestly, I wouldn't worry about this. Indentation never got in the way of Python's success. There are plenty other things to worry about besides this.
giancarlostoro 13 hours ago [-]
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.
AdieuToLogic 3 hours ago [-]
> 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.
And I love that people love indentation based languages so I show them a file with some spurious tabs to see how they feel about indentation causing silent errors.
sqlserver2008 6 hours ago [-]
Sure but even with no code indentation at all, an auto-formatter can easily indent everything for you because of the braces. If you have poorly indented code in a language like Python, you're on the hook for indenting everything yourself. And as a bonus, the code won't even run until you do.
koolala 13 hours ago [-]
Isn't it easy to just auto format it?
giancarlostoro 5 hours ago [-]
You mean add indentation to code where it shouldn't matter?
koolala 2 hours ago [-]
We need auto-unformatting too? Auto formatting that doesn't get added as a git change?
46 minutes ago [-]
NuclearPM 10 hours ago [-]
Use case. Not “user case”.
Verdex 15 hours 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 10 hours 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 8 hours 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 8 hours 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 7 hours 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.
cyanregiment 7 hours ago [-]
> These days I'm just glad they tolerate linq expressions and typescript
If it walks like a duck, farts like a dog, and flies like a fish - it's Java$cript.
TypeScript is used by the pious - they think it will bring them closer to God.
> dwarf fortresses that prove code with math
And then there's you guys.
Gattir allar,
aþr gangi fram,
vm scoðaz scyli,
vm scygnaz scyli;
þviat ouist er at vita,
hvar ovinir sitia
a fleti fyr
_doctor_love 4 hours ago [-]
Breathes there the man, with soul so dead,
Who never to himself hath said,
This is my own, my native land!
Whose heart hath ne’er within him burn’d,
As home his footsteps he hath turn’d,
From wandering on a foreign strand!
If such there breathe, go, mark him well;
For him no Minstrel raptures swell;
High though his titles, proud his name,
Boundless his wealth as wish can claim;
Despite those titles, power, and pelf,
The wretch, concentred all in self,
Living, shall forfeit fair renown,
And, doubly dying, shall go down
To the vile dust, from whence he sprung,
Unwept, unhonour’d, and unsung.
galangalalgol 3 hours ago [-]
How does this relate to the topic? I'm willing to assume it does, I just don't get it. I'm probably overreacting because when Scott was writing this, tens of thousands of Scots living in poverty were being evicted via arson from their land and country. Saying they were dead in spirit is very elitist as he sat in comfort.
kasumispencer2 13 hours 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?
giancarlostoro 13 hours ago [-]
Should be on the home page of any programming language site.
kasumispencer2 13 hours 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 11 hours ago [-]
There's a difference, yes. How big it is isn't really relevant question cause its simply an unnecessary tax on visitors.
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:
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 13 hours 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 10 hours 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 10 hours 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
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.
cyanregiment 9 hours ago [-]
> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].
Ok, what kinds of problems are they?
And ideally - what does a simple solution look like in F-star?
Set me on the path to installing the thing (ideally above the fold)
aleph_minus_one 8 hours ago [-]
> Ok, what kinds of problems are they?
> And ideally - what does a simple solution look like in F-star?
RTFM
Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.
> Set me on the path to installing the thing (ideally above the fold)
3. Download F* for an operating system of your choice there.
a1j9o94 3 hours ago [-]
You are right that someone could go through that effort bat that only really makes sense if they give you some.idea how to use it.
Reading the exchange it seems like you got caught up on the illustrative examples the other person used. If a web server isn't a good example of a simple problem for F* the landing page should have an example of something that is. It shouldn't take going through that many steps to understand the so what.
rainyq 15 hours ago [-]
just click the screenshot
cyanregiment 14 hours ago [-]
Takes you to an empty editor with still no code examples
remywang 13 hours ago [-]
That’s because syntax is the least interesting part of F*.
thomastjeffery 13 hours 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 13 hours 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*":
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.
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.
qzzi 15 hours ago [-]
I clicked on 2 links on the main page in the Learn F* section...
14 hours ago [-]
voodooEntity 12 hours ago [-]
Thank you ! I just had the absolute same experience and was about to write a similar comment - take my upvote instead !
summarity 10 hours ago [-]
What? There’s literally a completely interactive book linked right from the home page.
vivzkestrel 11 minutes ago [-]
- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust
pvsnp 16 hours ago [-]
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
rixed 13 hours ago [-]
What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?
aw1621107 6 hours ago [-]
I think it's meant to be parsed as "I liked being able to (express (calling external libraries))", not "I liked being able to (express calling) (external libraries)"
I guess responsive stylesheets can't be implemented without side effects...
3lambda 14 hours ago [-]
Would this language be useful for implementing compilers and formally proving things about them?
_thejanus_ 34 minutes ago [-]
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
dnautics 8 hours ago [-]
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.
_thejanus_ 55 minutes ago [-]
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
nickpsecurity 3 hours ago [-]
They started out that way. Keeping consistency between the formal specification and the code was always difficult. The further apart they are in distance or notation, the more difficult it is. So, the field experimented with verificatiom-oriented languages to localize changes.
physPop 11 hours ago [-]
yes thats the main reason, agda , coq similar ideas
_doctor_love 8 hours ago [-]
Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?
_thejanus_ 2 hours ago [-]
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.
IshKebab 14 hours ago [-]
F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out.
Does it get basic stuff like subtraction and u8 right, unlike Lean?
> But it doesn’t lead to confusion when doing mathematics in a theorem prover.
This is demonstrably untrue.
In any case that post is pretty unpersuasive. Basically saying it's too tedious to do it right, in a language whose whole purpose is tediously doing things right!
Probably the better conclusion is that more proof automation is needed for simple things like "this number is not negative" so it is less tedious.
(I'm not a Lean expert but I was totally put off by it happily accept a uint8 with value 300.)
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
Underappreciated benefit of side benefit of indentation based languages: no copy-pasta.
Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).
I think rixed means "code editing" (I guess that rixed is simply not a native (L1) or excellent L2 English speaker).
I find it easy to see if things are on the same indentation. I find it much harder to visually scan for opening and closing braces unless syntax highliting makes them scream at me or they are accompanied by ...indentation.
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.)
I think I need to see an example.
Perhaps English is not a native language for zlsa?
And I love that people love indentation based languages so I show them a file with some spurious tabs to see how they feel about indentation causing silent errors.
Also
> if you've worked with other proof oriented languages.
That's doing a lot of heavy lifting.
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).
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.
If it walks like a duck, farts like a dog, and flies like a fish - it's Java$cript.
TypeScript is used by the pious - they think it will bring them closer to God.
> dwarf fortresses that prove code with math
And then there's you guys.
Gattir allar,
aþr gangi fram,
vm scoðaz scyli,
vm scygnaz scyli;
þviat ouist er at vita,
hvar ovinir sitia
a fleti fyr
Who never to himself hath said,
This is my own, my native land!
Whose heart hath ne’er within him burn’d,
As home his footsteps he hath turn’d,
From wandering on a foreign strand!
If such there breathe, go, mark him well;
For him no Minstrel raptures swell;
High though his titles, proud his name,
Boundless his wealth as wish can claim;
Despite those titles, power, and pelf,
The wretch, concentred all in self,
Living, shall forfeit fair renown,
And, doubly dying, shall go down
To the vile dust, from whence he sprung,
Unwept, unhonour’d, and unsung.
But I clicked one (1) link to the online book and found a thousand?
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-oriented-programming-i...
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!
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.
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
> 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.
Ok, what kinds of problems are they?
And ideally - what does a simple solution look like in F-star?
Set me on the path to installing the thing (ideally above the fold)
> And ideally - what does a simple solution look like in F-star?
RTFM
Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.
> Set me on the path to installing the thing (ideally above the fold)
How to install this thing:
1. Read https://fstar-lang.org/index.html#download
2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases
3. Download F* for an operating system of your choice there.
Reading the exchange it seems like you got caught up on the illustrative examples the other person used. If a web server isn't a good example of a simple problem for F* the landing page should have an example of something that is. It shouldn't take going through that many steps to understand the so what.
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-i...
> https://fstar-lang.org/tutorial/
Edit: For comparison, Rocq https://rocq-prover.org/ and Lean https://lean-lang.org/ both manage to do this.
Is this used in the industry ? And for what kind of software ?
Some Windows things too I think (I think F* is partially funded by Microsoft Research)
They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementations
https://project-everest.github.io/
https://github.com/hacl-star/hacl-star
https://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)
https://www.microsoft.com/en-us/research/blog/everparse-hard...
https://lwn.net/Articles/770750/
https://project-everest.github.io/
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
Does it get basic stuff like subtraction and u8 right, unlike Lean?
This is demonstrably untrue.
In any case that post is pretty unpersuasive. Basically saying it's too tedious to do it right, in a language whose whole purpose is tediously doing things right!
Probably the better conclusion is that more proof automation is needed for simple things like "this number is not negative" so it is less tedious.
(I'm not a Lean expert but I was totally put off by it happily accept a uint8 with value 300.)
> No, it isn't.
https://fstar-lang.org/ claims otherwise:
"F* (pronounced F star)".