Hacker News Reader

Comment by keyle | Hacker News Reader

I'm confused. Is this either very new or very old? What's the context?

F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of programs (say that qsort actually sorts, or that a tree is balanced and implements a mathematical map).

Typically such languages are more academic than F*.

I would also say take a look at Bosque it is also from the same camp as F* but much simpler to use Z3 with.

i am not familiar with fstar. But I will try to provide some context badly so someone who does know it can correct me.

Javascript is dynamically typed, and so has no type checking until runtime, you don't know whether a passed in parameter is a string or not until you try to use it.

C# is statically typed, so the compiler knows whether something is a string when passed in at compile time, not making you wait until runtime.

Ocaml/F# have a stronger type system than c#, so you get the compiler looking for you not only that something is a string, but that it is a named type like fifteenString, which is a string with a length of always 15 characters.

F* takes this even further, where the compiler checks for you that you've passed in a fifteenString and that it matches criteria in its value like "starts with hello" or "does not contain bye".

C# saves you from needing to check if a param is even a astring at runtime.

F# additionally saves you from needing to check if it is null and 15 characters in length at runtime.

F* additionally saves you needing to check its value starts with hello at runtime.

Again this is a single language feature probably poorly explained!

The only difference between F# and C# with respect to the notion of a "type which represents a string of length 15" is the amount of code to do it - as described by Scott Wlaschin [1]. You could do the equivalent in C# too. I don't know if this is also the case in Ocaml, though.

[1]: https://fsharpforfunandprofit.com/posts/designing-with-types...

Ocaml beginner here, didn't know you could restrict an Ocaml type to a string of a given length !! How would you go about that ?? Cheers :)

The easiest way is probably to define a private subtype of string (type small_string = private string) with smart constructors that enforces the restriction at runtime. This often means that creating such values may fail, but if you have a value of this type you are assured that the constraint on the size holds.

As pointed out by dang, the same (I think) tutorial was discussed in 2016 (https://news.ycombinator.com/item?id=10949288). I went through the first half of the tutorial in 2018, and I think some aspects of F* were genuinely new, but the development seems to have stopped. There is a need for a framework for program verification of real-life software by non-experts, but F* might not be it. In the latest article [1] of Project Everest one can read: "[...], it required several person-months to implement and verify a generic doubly-linked list library in F*, while it required only three hours to do so in Dafny."

[1] A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou) To Appear In The Proceedings of the 42nd IEEE Symposium on Security & Privacy 2021.

  it required several person-months to implement and verify a generic doubly-linked list library in F*, while it required only three hours to do so in Dafny

This could be deceptive. Structures like linked-lists are fiendishly hard to implement in safe Rust too, but people are able to stay productive by (mostly) not implementing things like that themselves. In Rust's case the difficulty comes from ownership: anything involving complex reference graphs for the sake of traversal is going to be really gnarly to establish a single-ownership story for. I don't know about F*.

According to the F* landing page [1]:

> F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification.

> The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest [2]. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives.

[1] http://www.fstar-lang.org/

[2] https://project-everest.github.io/

Fairly new language.

Reply on news.ycombinator.com