HN Explorer

17 comments

[ 1.6 ms ] story [ 25.3 ms ] thread
pvsnp
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
cyanregiment
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

3lambda
Would this language be useful for implementing compilers and formally proving things about them?
_thejanus_
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
IshKebab
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?

boutell
I guess responsive stylesheets can't be implemented without side effects...
LelouBil
I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.

Is this used in the industry ? And for what kind of software ?

_doctor_love
Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?
_thejanus_
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.
vivzkestrel
- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust
mxkopy
Julia is basically this, i.e. compiled typed python. The nesting for type declarations gets gnarly though, which answers your general question - the really nice language ergonomics cost compute at runtime because that’s the only way you avoid laying everything out beforehand.