4 ms·

F* reworked and released as v0.9.0

• ahelwer 11y ago
  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?
  • platz 11y ago
    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."
    • platz 11y ago
      it looks like they are able to reference mscorlib https://github.com/FStarLang/FStar/blob/997b1f20f35142e650325da7054a37f425ad1b00/old/to_be_ported/sep/prims-sep.fst#L188 https://github.com/FStarLang/FStar/blob/997b1f20f35142e65032... and F# with these externs https://github.com/FStarLang/FStar/blob/997b1f20f35142e650325da7054a37f425ad1b00/old/to_be_ported/pldi10-benchmarks/lookout/externs.fine#L8 https://github.com/FStarLang/FStar/blob/997b1f20f35142e65032...
      • jaked89 11y ago
        This code exists in a folder named "old/to_be_ported", which might indicate that it no longer functions. It appears that the correct way is to create a .fsi file. A few examples: https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.diagnostics.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.text.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.collections.generic.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba... https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba221b1f354216218cd397/lib/system.io.fsi https://github.com/FStarLang/FStar/blob/4e4162f736195b2031ba...
        • platz 11y ago
          ahh, good catch
• deleted 11y ago
  [deleted]
• CoffeeDregs 11y ago
  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
  • nickpsecurity 11y ago
    It says what it does in the linked article with examples like refinement types. The comments section had these two videos from them as well: https://www.youtube.com/watch?v=bEJKKquyngk https://www.youtube.com/watch?v=bEJKKquyngk https://www.youtube.com/watch?v=em_tDc1Gc40 https://www.youtube.com/watch?v=em_tDc1Gc40