F* is a verification-oriented programming language developed at Microsoft Research. If you already know F#, or OCaml, or Haskell, or another language from ML family, you’ll find it familiar.
To start experimenting with the language on your machine you need .NET 4.0. With Windows that’s it – just start enjoying verifications. But things are getting more interesting if you’re a mono user, when you want to compile the “right” compiler with blackjack and everything.
F* Download includes the sources and some binaries to bootstrap the compiler.
There is a dependency on Z3, we need F# PowerPack libs, fslex, fsyacc and i386 version of dylib for Mac and mono version of
Microsoft.Z3.dll library (either compile a new one or download here or here).
But first of all, need to admit it works only for the small programs now. That’s why I ain’t gonna list the steps now. They are actually quite straightforward – update the paths 1 and fix the errors if any (e.g. I replaced the reserved word
cnst). You can also define
MONO symbol and add references to
The first wall is
Certify.dll rule – got StackOverflow here. Given the .dll which is in bin folder by default, everything else compiles, including
At this point only the simplest programs can be successfully verified. Why only them?
F* relies on tail call optimizations – lots and lots of recursive functions here. Consider the following simple function, it does nothing usefull but illustrates the problem:
We can verify that the
.tail instructions are where expected:
Does it work? Well, for .NET the answer is yes. But on mono the continuation part makes the stack grow. Manipulations with stack size are not the solution, so the sources modification seems to be a way to go.
There’s an old issue with tail calls when called and caller functions have different number of parameters. I thought that can be the case, because of
InvokeFast methods, and created a special type for arguments, so all functions had a single parameter. It isn’t.
I still believe it is possible to get F* working on mono 2. Hope to find some spare time to dig into the logic and check how it can be rewritten with a simpler recursion, just extremely busy right now ). I also shared some ideas with Nikhil Swamy from F* team – he experimented with mono builds too and definitely knows much better what can be done. That’s an interesting challenge and, of course, the fresh ideas are very welcome!