On 24 August 2017 we released F* v0.9.5.0. This is another big release with lots of changes and new features compared to v0.9.4.0.

Main new features

  • Proofs by reification (see this paper)
  • A revision of the libraries based on a new formal account of monotonic state (see this paper)
  • Extraction of programs with user-defined effects
  • Experimental support for tactics
  • New IDE protocol and new IDE features: autocompletion, evaluation, real-time syntax checking, jump-to-definition, type-at-point, etc.

Changes and other improvements

  • A reorganization of the library and a single fstarlib.cmxa against which to link all F* programs compiled to OCaml (this change is incompatible with previous versions of F*)
  • A new printer of source terms
  • Revised error reporting from failed SMT queries
  • Improved support for separate compilation via a binary format for checked modules
  • Fixed a ton of bugs (179 closed GitHub issues)