# Introduction

F* (pronounced

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 POPL 2016 paper and
a more recent draft.
You can learn more about F* by following the online
tutorial.
Materials from recent talks are
available below.

The main ongoing use case of F* is building a
verified, drop-in replacement for the whole HTTPS stack in
Project Everest.
This includes verified implementations of
TLS 1.2 and 1.3 and
elliptic curve cryptography.
Moreover, while F* is extracted to OCaml by default, we are devising
a subset of F* that can be
compiled to C for efficiciency.

Previous versions of F* could also be translated to JavaScript.
We have used these previous versions in a number of projects, ranging from
verifying implementations of cryptographic constructions and protocols,
implementations of web browser extensions,
formalizing the semantics of other languages
(including
JavaScript and a compiler from a subset of F* to JavaScript,
and
TS*, a secure subset of TypeScript),
and even
certifying the correctness of the core of F* type-checker itself.