F* reworked and released as v0.9.0

I'm excited about the release of any functional-ish language, but I'm unclear as to how F* is different from F# or OCaml. I did read some of the docs, but any pointers?

I should have read more:

    We aim for a language that spans the capabilities of interactive proof
    assistants like Coq and Agda, general-purpose programming
    languages like OCaml and Haskell, and SMT-backed semiautomated
    program verification tools like Dafny and WhyML. This language
    would provide the nearly arbitrary expressive power of a logic
    like Coq’s, but with a richer, effectful dynamic semantics.
    It would provide the flexibility to mix SMT-based automation
    with interactive proofs when the SMT solver times out (not uncommonly
    when working with rich theories and quantifiers). And it would
    support idiomatic higher-order, effectful programming with the
    predictable, call-by-value cost model of OCaml, but with the
    encapsulation of effects provided by Haskell.

That sounds pretty exciting. Especially considering you can use the full .NET stack (which I'm not currently using (Linux) but definitely respect).

EDIT: formatting

Does anyone know how well F* interacts with the .NET framework, if at all? Or unverified code in general? Can you "wall off" the unverified code by stating a bunch of assumptions about how it works?