hannes.robur.coop/About

---
title: About
author: hannes
tags: overview, myself, background
abstract: introduction (myself, this site)
---

## What is a "full stack engineer"?

Analysing the word literally, we should start with silicon and some electrons,
maybe a soldering iron, and build everything all the way up to our favourite
communication system.

While I know how to solder, I don't plan to write about hardware in here.  I'll
assume that off-the-shelf hardware (arm/amd64) is available and trustworthy.
Read the [Intel x86 considered
harmful](http://blog.invisiblethings.org/papers/2015/x86_harmful.pdf) paper in
case you're interested in trustworthiness of hardware.

My current obsession is to enable people to take back control over their data:
simple to setup, secure, decentralised infrastructure.  We're not there yet,
which also means I've plenty of projects :).

I will write about my projects, which cover topics on various software layers.

### Myself

I'm Hannes Mehnert, a [hacker](http://www.catb.org/jargon/html/H/hacker.html)
(in the original sense of the word), 3X years old.  In my spare time, I'm not
only a hacker, but also a barista.  I like to travel and repair my recumbent
bicycle.

Back in 199X, my family bought a PC.  It came
with MS-DOS installed, I also remember Windows 3.1 (likely on a later computer).
This didn't really hook me into computers, but over the years I started with
friends to modify some computer games (e.g. modifying text of Civilization).  I
first encountered programming in high school around 1995: Borland's Turbo Pascal
(which chased me for several years).

Fast forwarding a bit, I learned about the operating system Linux (starting with
SUSE 6.4) and got hooked (by providing basic network services (NFS/YP/Samba)) to
UNIX.  In 2000 I joined the [Chaos Computer Club](https://www.ccc.de).
Over the years I learned various things, from Linux kernel modifications,
Perl, PHP, basic network and security.  I use [FreeBSD](https://www.FreeBSD.org) since 4.5, FreeBSD-CURRENT
on my laptop.  I helped to [reverse engineer and analyse the security of a voting
computer](http://wijvertrouwenstemcomputersniet.nl) in the Netherlands, and some
[art installations](http://blinkenlights.net/) in Berlin and Paris.  There were
several annual Chaos Communication Congresses where I co-setup the network
(backbone, access layer, wireless, network services such as DHCP/DNS), struggling with
Cisco hardware from their demo pool, and also amongst others HP, Force10, Lucent, Juniper
equipment.

In the early 200X I started to program [Dylan](https://opendylan.org), a LISP
dialect (dynamic, multiple inheritance, object-oriented), which even resulted in
a [TCP/IP
implementation](https://github.com/dylan-hackers/network-night-vision/)
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
[gradually typed](http://homes.soic.indiana.edu/jsiek/what-is-gradual-typing/)
Dylan would look like, leading to my master thesis.  Gradual typing is the idea to evolve untyped programs into typed 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://mirageos.org), 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.

From summer 2014 until end of 2017 I worked as a postdoctoral researcher at University of Cambridge (in the [rigorous engineering of mainstream systems](https://www.cl.cam.ac.uk/~pes20/rems) project) with [Peter Sewell](https://www.cl.cam.ac.uk/~pes20/).  I primarily worked on TLS, MirageOS, opam signing, and network semantics.  In 2018 I relocated back to Berlin and am working on [robur](http://robur.coop).

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).

The data of this blog is [stored in a git repository](https://git.robur.coop/hannes/hannes.robur.coop).