Table of Contents
1 How to Comfortably use F*
All these features culminate in a high level language that excels at verifying and generating low level code. Although F* has been used to achieve wondrous results, actually learning the language and becoming comfortable in it is quite challenging.
This post thus seeks out to remedy common gotchas I came across while learning F*. Future posts will be dedicated to explaining various parts of the STDLib and how the OCaml extraction works.
- I would read the introduction section of the tutorial to get a good
feel for the language.
- Great thing about this tutorial, is that it already has an editor setup for verifying code.
- I would also suggest getting familiar with OCaml, at least enough to be able to read.
- I would then install F*.
Opamis the easiest, however you will also need to install
Z3for your system as well
- This requires a working version of OCaml between 4.04 and 4.08 ([4.04, 4.08)).
- Then setup your editor This post will assume you are using
emacsas that has the most mature editing mode.
- I also suggest playing around with the listed keybindings.
- Be comfortable with
Emacsbindings, in this post I will often say
C-cbto mean Control-c Control-b
1.2 Into the Deep End
Great, Now that
F* is now installed on your system, we can begin to
explore various pain points surrounding development and learning.
1.2.1 Tutorial Issues
The tutorial is the best place to learn
F*, however the tutorial is
far from perfect. Often the included code is outdated and will not
This issue is most pronounced in section
2.3.2 which shows the
following seemingly harmless piece of code
open FStar.All open FStar.List.Tot open FStar.Ref val new_counter: int -> St (unit -> St int) let new_counter init = let c = ST.alloc init in fun () -> c := !c + 1; !c
If you were to try to verify this code, they would get
not prove psot-condition. This is not because the type signature is
incorrect but due to an issues which can be seen here, here, and here.
Other issues include having old type signatures or missing pieces of
code, so if any example does not verify in your editor, I would highly
suggest to scroll down to the nearest exercise and click
editor. These code snippets are up to date and should not fail at
1.2.2 Emacs Mode Issues And Tips
Similarly to the tutorial, Emacs's Fstar-mode is the most mature mode
F* but has its own share of problems that one has to learn to
- No longer allowed to import new modules
One issue I often face, is that I start to verify a buffer (I start this with
C-cn[verify next statement!]) and add in new definitions. Starting to verify a new buffer causes
fstar.exeto be a long living process. When this process starts, it starts to verify all imported libraries at the module name.
What this means is that if you were to suddenly require a new dependency say
FStar.HyperStackyou would get the error
Namespeace FStar.HyperStack cannot be foundeven though it is clearly in the standard library.
This is fixed by simply pressing
C-cxto kill the long living process and start a new none, re-verifying the entire buffer
This isn't the most ideal solution, however this can be dramatically sped up by using verified cached modules.
- Getting into an Invalid State
There are a few keys in the emacs mode that may cause the verifier to give an invalid state.
One way I often triggered this was by pressing
C-c<enter>. These commands verify up until your cursor. If your cursor is in the middle of syntax this will likely cause a parse error. The best action is to only use these commands where you cursor is not in the way of any text and rely on
C-cninstead to verify the next statement and
C-cpto unverify the last statement
- Invalid Verified Code
- There are times when the
Emacsmode will verify statements which may be invalid. For the sake of simplicity, put the
2.3.2code in the Tutorial Issues section into a new blank files, and run
C-cl. Notice that the code verifies perfectly! A trick to get around this is either to
C-cnthe whole file (this may be time consuming), or to press
C-c<enter>at the bottom of the file. These seem to not have the issues
- There are times when the
- Running code without generating OCaml code
The emacs mode comes with the key combination
C-cse, which allows the user to run any verified piece of code!
This can come in handy if one doesn't feel like generating OCaml and running it in their file
- Getting type definitions of unfinished definitions
- One annoying thing about
F*is that error messages tend to be opaque. So one trick I've found is to write a function, then put the hole
admit ()somewhere in the code and see what base signature it requires. This is gotten by
C-csp. Note that this isn't always the nicest way to get type signatures as it expands
STinto the full blown
Statewhich can be quite intimidating.
- One annoying thing about
1.2.3 Sharing OCaml and F* code
One of the nicer things about
F*, is that the translation to
is very straightforward.
However one issue Ι originally had was how does this work? a
post on the F* wiki shows an easy way to achieve this. However, it wasn't
clear if this was only for the
F* ∩ OCaml ∩ F# subset of
Thankfully, it turns out that this also works for just normal
Create a fsti file for an interface, say
(* Getopt.fsti *) (* Taken from F* source code *) module Getopt open FStar.ST open FStar.All open FStar.Pervasives val noshort : Char.char val cmdline: unit -> list string
F#instantiation of this code, with ints replaced with Z.t
(* GetOpt.ML *) let noshort = 0 (* ... *) let cmdline () = Array.to_list (Sys.argv)
F*code which relies on this interface
(* Useage.fst *) module Useage open Getopt let test = cmdline
F* will happily verify and produce
Useage.ml for you.
1.2.4 Build Scripts and Environments
Note that a build script is very helpful for the above code, because
.ml files for every single used library in
the current directory.
This is not only slow, but it also clutters the directory. The wiki
has a good post covering how to deal with this, however Ι could not
get the build script it points to work.
So instead I made this bash script that can be augmented to allow STDLib caching among other improvements that can be made
fstar.exe $1 --codegen OCaml \ --no_extract FStar.Pervasives.Native \ --no_extract FStar.Pervasives \ --no_extract FStar.Mul \ --no_extract FStar.Preorder \ --no_extract FStar.Calc \ --no_extract FStar.StrongExcludedMiddle \ --no_extract FStar.List.Tot.Base \ --no_extract FStar.List.Tot.Properties \ --no_extract FStar.List.Tot \ --no_extract FStar.Seq.Base \ --no_extract FStar.Seq.Properties \ --no_extract FStar.Seq \ --no_extract FStar.Math.Lib \ --no_extract FStar.Math.Lemmas \ --no_extract FStar.BitVector \ --no_extract FStar.UInt \ --no_extract FStar.UInt32 \ --no_extract FStar.UInt64 \ --no_extract FStar.UInt8 \ --no_extract FStar.PropositionalExtensionality \ --no_extract FStar.PredicateExtensionality \ --no_extract FStar.TSet \ --no_extract FStar.Heap \ --no_extract FStar.ST \ --no_extract FStar.IO \ --no_extract FStar.All \ --no_extract FStar.Exn
Thus one can just run this shell script on a
.fst file and get the
Another piece of data that is needed to run the outputted
code, is to load this into a toplevel with
#require "fstarlib";;. I
simply put this line in my
~/.ocamlinit, but you could of course put
this in the toplevel manually.
1.3 Final Words
F* is a rather fun language, however it has a lot of unique quirks
that must be programmed around. Hopefully this blog post has helped
you avoid some of them.
Interested in Programming Language Theory & Type Theory? Metastate is hiring, check out our Functional Compiler Engineer position and our [Type Theorist & Formal Verification Engineer position]https://metastate.dev/join/).