Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • 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

    by cyanregiment
  • That’s because syntax is the least interesting part of F*.
    by remywang
  • I clicked on 2 links on the main page in the Learn F* section...
    by qzzi
  • just click the screenshot
    by rainyq
  • Two clicks take you to the tutorial: https://fstar-lang.org/tutorial/
    by bmitc
  • https://fstar-lang.org/tutorial/
    by munchler
  • > Clicked like 5 pages and never found 1 code example.

    But I clicked one (1) link to the online book and found a thousand?

    by kasumispencer2
  • 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.
    by Verdex
  • 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.
    by rixed
  • I guess responsive stylesheets can't be implemented without side effects...
    by boutell
  • Would this language be useful for implementing compilers and formally proving things about them?
    by 3lambda
  • yes thats the main reason, agda , coq similar ideas
    by physPop
  • 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.
    by dnautics
  • 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
    by _thejanus_
  • Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?
    by _doctor_love
  • 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.
    by _thejanus_
  • - stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust
    by vivzkestrel
  • 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.
    by mxkopy
  • There's nim [1] which is aiming for the same thing - syntax similar to python and performance similar to C++, zig etc.

    1 - https://nim-lang.org/

    by DedlySnek
  • That language is basically F#, except for perhaps the performance claims. But F# is definitely not a slow language.
    by bmitc
  • Your question is why don't we have a language that performs much better than the best-performing languages? Why would you expect such a thing?
    by fluoridation
  • 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 ?

    by LelouBil
  • I found these links in the F* book

    https://www.microsoft.com/en-us/research/blog/everparse-hard...

    https://lwn.net/Articles/770750/

    https://project-everest.github.io/

    by LelouBil
  • Firefox cryptographic primitives are written and formally verified in F*

    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)

    by nextaccountic
  • 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?

    by IshKebab
  • https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
    by gugagore
  • https://fstar-lang.org/tutorial/
    by LelouBil
  • I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
    by pvsnp
  • What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?
    by rixed