The F* team is pleased to announce the release of F* v0.9.4.0. This is the culmination of exactly one year of hard work from a very quickly expanding F* team. We’re not very good at keeping precise change lists, but here are the main highlights of this release:

  • Predicative hierarchy of universes with universe polymorphism
  • Uniform syntax between expressions and types allowing rich type-level computation
  • Dijkstra Monads for Free
  • Extraction to C via KreMLin
  • New parser based on Menhir
  • New pretty printer for surface syntax and fstar --indent
  • Changed default effect to Tot
  • Strict positivity check for inductives
  • New synatax for inductive type projectors and discriminators
  • Better semantics for module open and support for local opens
  • Better dependency analysis
  • Better error locations for Z3 failures
  • Replaced Z3 timeouts with machine independent resource limits
  • Cleaned up libraries and examples (a bit)
  • Improvements to interactive mode
  • Docker builds
  • Fixed a ton of bugs (262 closed GitHub issues)

Enjoy the best F* release ever!