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.cmxaagainst 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)