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.

[Originally posted here].

###Resources:

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 const with cnst). You can also define MONO symbol and add references to z3mono.dll.

The first wall is Certify.dll rule – got StackOverflow here. Given the .dll which is in bin folder by default, everything else compiles, including fstar.exe.

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:

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
let rec f x cont =                                                       
    if x < 0 then 0
    elif x = 0 then cont x
    else f (x-1) (fun x -> f x cont)

f 250000 id //SO

We can verify that the .tail instructions are where expected:

 1: 
 2: 
 3: 
 4: 
 5: 
 6:   

 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27:   

28: 
29: 
30: 
31: 
32: 
33: 
34:   

35: 
36: 
37: 
38: 
39: 
.method public static 
  int32 f (int32 x,
	 class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> cont
	 ) cil managed	
{	
 .custom instance void [FSharp.Core]Microsoft.FSharp.Core
	.CompilationArgumentCountsAttribute::.ctor(int32[]) = (
		01 00 02 00 00 00 01 00 00 00 01 00 00 00 00 00
	)
	// Method begins at RVA 0x2050
	// Code size 35 (0x23)
	.maxstack 8
	// loop start
	 IL_0000: nop
	 IL_0001: ldarg.0
	 IL_0002: ldc.i4.0
	 IL_0003: bge.s IL_0007
  
	 IL_0005: ldc.i4.0
	 IL_0006: ret
  
	 IL_0007: ldarg.0
	 IL_0008: brtrue.s IL_0014
  
	 IL_000a: ldarg.1
	 IL_000b: ldarg.0
	 IL_000c: tail.  // cont x
	 IL_000e: callvirt instance !1 class 
           [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>::Invoke(!0)
	 IL_0013: ret
  
	 IL_0014: ldarg.0
	 IL_0015: ldc.i4.1
	 IL_0016: sub
	 IL_0017: ldarg.1
	 IL_0018: newobj instance void Tailcalls/f@4::.ctor(
           class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>) 
	 IL_001d: starg.s cont
	 IL_001f: starg.s x
	 IL_0021: br.s IL_0000
	 // end loop
}  // end of method Tailcalls::f
 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11:   

12: 
13:   

14: 
15: 
.method public strict virtual 
instance int32 Invoke (int32 x) cil managed 
{
	// Method begins at RVA 0x2084
	// Code size 16 (0x10)
	.maxstack 8

	IL_0000: nop
	IL_0001: ldarg.1
	IL_0002: ldarg.0
	IL_0003: ldfld class 
          [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> Tailcalls/f@4::cont
	IL_0008: tail.  // f x cont
	IL_000a: call int32 Tailcalls::f(int32, 
          class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>)
	IL_000f: ret
}  // end of method f@4::Invoke

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 FSharpFunc Invoke/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!

 

val f : int -> (int -> int) -> int

Full name: Test.f

val x : int

type: int
implements: System.IComparable
implements: System.IFormattable
implements: System.IConvertible
implements: System.IComparable<int>
implements: System.IEquatable<int>
inherits: System.ValueType

val cont : (int -> int)

val id : 'T -> 'T

Full name: Microsoft.FSharp.Core.Operators.id

  1. it’s better to include the full paths – for example I usually happily forget that fsc on my machine means Fast Scala Compiler and waste the time trying to get why it rejects .fs files.

  2. everything comes to electricity at the end, right? ;)

How to Name a Cat

A fun conversation about mountains, monads, types and heels reminded me about the first University years and one of our favourite math jo...… Continue reading

Keywords Mix

Published on March 15, 2016

Traditions vs Statistics: Sechseläuten

Published on April 25, 2015