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).
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?
according to the tutorial "F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform file input/output are implemented by the operating system and made available to F* programs via the underlying framework, e.g., .NET or OCaml."
I should have read more:
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