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

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