including a wireshark-like GTK based user interface with a shell similar to IOS for configuring the stack.
I got excited about programming languages and type theory (thanks to
[types and programming languages](https://www.cis.upenn.edu/~bcpierce/tapl/), an
excellent book); a key event for me was the [international conference on functional programming (ICFP)](http://cs.au.dk/~danvy/icfp05/). I wondered how a
Dylan would look like, leading to my master thesis. Gradual typing is the idea to evolve untyped programs into types ones, and runtime type errors must be in the dynamic part. To me, this sounded like a great idea, to start with some random code, and add types later.
My result was not too convincing (too slow, unsound type system).
Another problem with Dylan is that the community is very small, without sufficient time and energy to maintain the
self-hosted compiler(s) and the graphical IDE.
During my studies I met [Peter Sestoft](http://www.itu.dk/people/sestoft/).
After half a year off in New Zealand (working on formalising some type systems),
I did a PhD in the ambitious research project "[Tools and methods for
scalable software verification](https://itu.dk/research/tomeso/)", where we mechanised proofs of the functional correctness
of imperative code (PIs: Peter and [Lars Birkedal](http://cs.au.dk/~birke/)).
The idea was great, the project was fun, but we ended with 3000 lines of proof
script for a 100 line Java program. The Java program was taken off-the-shelf,
several times refactored, and most of its shared mutable state was removed. The
proof script was in [Coq](https://coq.inria.fr), using our higher-order separation logic.
I concluded two things: formal verification is hard and usually not applicable
for off-the-shelf software. *Since we have to rewrite the software anyways, why
not do it in a declarative way?*
Some artefacts from that time are still around: an [eclipse plugin for
Coq](https://coqoon.github.io/), I also started (with David) the [idris-mode for
emacs](https://github.com/idris-hackers/idris-mode). Idris is a dependently
typed programming language (you can express richer types), actively being
researched (I would not consider it production ready yet, needs more work on a
faster runtime, and libraries).
After I finished my PhD, I decided to slack off for some time to make decent
espresso. I ended up spending the winter (beginning of 2014) in Mirleft,
Morocco. A good friend of mine pointed me to [MirageOS](https://mirage.io), a
clean-slate operating system written in the high-level language [OCaml](https://ocaml.org). I got
hooked pretty fast, after some experience with LISP machines I imagined a modern
OS written in a single functional programming language.
MirageOS had various bits and pieces into place, including infrastructure for
building and testing (and a neat self-hosted website). A big gap was security.
No access control, no secure sockets layer, nothing. This will be the topic of
another post.
OCaml is [academically](http://compcert.inria.fr/) and [commercially](https://blogs.janestreet.com/) used, compiles to native code (arm/amd64/likely more), is
fast enough ("Reassuring, because our blanket performance statement 'OCaml
delivers at least 50% of the performance of a decent C compiler' is
not invalidated :-)" [Xavier Leroy](https://lwn.net/Articles/19378/)), and the [community](https://opam.ocaml.org/packages/) is sufficiently large.
### Me on the intertubes
You can find me on [twitter](https://twitter.com/h4nnes) and on
[GitHub](https://github.com/hannesm). I also have an [academic web
site](https://www.cl.cam.ac.uk/~hm519/).
No comments here, but you can open issues on the [data repository on
