The functional-first style encouraged by F# rules out many simple bugs, but we’ve all struggled with deeper algorithmic bugs lurking in our programs. F* is a new research language from Microsoft Research that allows you to formally prove the full functional correctness of code written in a strict, higher-order, stateful programming language, e.g., programs in idiomatic F#, Caml and related languages. This tutorial will give you an overview of F*, including an introduction to the theory of dependent types that's at the heart of F* and the automated theorem-proving technology that underlies its implementation. You will write and formally prove the correctness of several small algorithms, data structures, and web programs. Get started with F* already! An interactive tutorial:http://rise4fun.com/FStar/tutorial/guide Links to several research papers and a compiler download: http://research.microsoft.com/en-us/projects/fstar/

No outline is available