I sure hope the aggregate effect of F*, ATS, Rust, and such is to more quickly bring about even better static checking.
v0.9.0 (released before ICFP 2015). Countless improvements, including an interactive mode, a new extraction mechanism to OCaml and F#, the ghost effect, a lot of new examples (micro-F* formalization, Wysteria, etc), hyper-heaps, build-config support, quite a bit of cleanup of the code base.
F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml or F# for execution.
The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source and under active development on GitHub. A detailed description of this new F* version is available in a recent draft. You can learn more about F* by following the online tutorial.
Recent comments
22 weeks 6 days ago
22 weeks 6 days ago
22 weeks 6 days ago
45 weeks 22 hours ago
49 weeks 2 days ago
51 weeks 1 hour ago
51 weeks 1 hour ago
1 year 1 week ago
1 year 6 weeks ago
1 year 6 weeks ago