4 ms·

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 bu

by 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

by 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