[ivarru]

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.

[brundolf]

  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*.