maintaining a logically consistent core; it enables modular reasoning about state and other effects using afﬁne types; and it supports proofs of reﬁnement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq)
and logical consistency for F*. We have implemented a compiler that translates F* to .NET
bytecode, based on a prototype for Fine. F* provides access to
libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. We have formalized the metatheory of F*, and mechanized a signiﬁcant part of the metatheory in Coq. We have developed a prototype compiler for F* (35,000 lines of F#), and used F* to program and verify more than 20,000 lines of code. We believe F* is the ﬁrst language of its kind with such a scale of implementation and evaluation.