Hello! It is my pleasure to announce that F* is once again available on opam for direct installation after a long time. This probably does not mean much to regular users, as there were regular releases on GitHub for some time now. However, the opam release offers a convenient alternative by eliminating the need to separately set up OCaml to compile extracted OCaml code.
From the website -
F* is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving.
The biggest new thing worth mentioning is perhaps the Pulse DSL for programming with concurrent separation logic. A tutorial is available in the F* book, Proof-oriented Programming in F*. A comprehensive overview of various projects that have utilized F* over the years can also be found on the website.
Feel free to join the Zulip forum for discussions with the developers, researchers, and casual users. Happy writing provably correct programs!