F★ Interfaces (simple version)

Interfaces & code generation

As of 02/12/2016, the only legitimate usage of an .fsti file is to indicate a series of definitions that will be automatically assumed by F*; a .fsti file generates no code at extraction-time. You have to provide, say, an OCaml implementation of the specified interface. For instance, FStar.IO.fsti generates no code; we provide an OCaml-specific implementation of it in lib/ml/FStar_IO.ml.

Some modules are written as .fst's; however, they are meant to be replaced at extraction-time by more efficient implementations. For these modules, you have to pass the --no-extract flag to make sure no code is generated at extraction-time. For instance, FStar.List.fst is replaced by Batteries' more efficient functions at extraction-time.

In the specific case of F*'s standard library, the following modules are implemented as .fst's but then realized: All Heap List Set. Furthermore, for convenience, we provide a single .cmxa for all the OCaml-implemented modules. Therefore, in your Makefile, you should do:

STDLIB_REALIZED=All Heap List Set
FSTARFLAGS=--codegen OCaml $(addprefix --no-extract ,$(STDLIB_REALIZED))

all: $(FSTFILES)
  $(FSTAR) $(FSTARFLAGS) $^
  $(MAKE) -C $(FSTAR_HOME)/lib/ml
  $(OCAML) $(FSTAR_HOME)/lib/ml/fstarlib.cmxa $(FSTFILES:.fst=.ml)

Note: ulib/ml/Makefile.include does this for you. Use it! (See examples/hello)

If you need to build and verify against hyperheaps, the recursive make invocation should be:

  $(MAKE) -C $(FSTAR_HOME)/lib/ml hyperheap PRIMS_DIR=native_int

Writing F★ code in a modular way

• Step 1: write out a series of assume val definitions in your file; this is the interface that other people in the project will program against.
• Step 2: play around; perhaps write a series of experimental functions in the same file.
• Step 3: once the playground stabilizes, start matching the interface that has been exposed earlier in the file. When a function verifies and matches against its val declaration, remove the assume keyword.

Note: two possible styles:

• write all the val's at the beginning of the file (kind of like an interface declaration); then, all the let's follow; this requires a tweak in F★ because val a: ... val b: ... mentions a ... doesn't work unless val a is either assume'd or followed by a corresponding let -- another drawback is that the programmer needs to jump around in his buffer to look up the val definitions
• keep the usual style where val is followed by a let; write a tool that is capable of dumping a readable "documentation file" (e.g. HTML or Markdown) from an .fst file

Use-case 1: I want to agree on an interface, then play around while others write code against said interface. Answer: use scenario above.

Use-case 2: We agreed on an interface, I have a partial implementation that --lax type-checks, but I still want others to be able to carry on with their lives. Answer: use val and let (no assume) but tell other people who depend on your module to use the --verify-module TheirModule argument so that your module is lax type-checked.

Use-case 3: TheirModule does not verify anymore but you want to carry on with your life and keep working on YourModule. Answer: revert their commit.

Use-case 4: I want to commit a sketch of ideas that doesn't even parse or lax type-check. Answer: use a text file.