About

Written by hannes
Classified under: overviewmyselfbackground
Published: 2016-04-01 (last updated: 2023-11-20)

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 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 (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. Over the years I learned various things, from Linux kernel modifications, Perl, PHP, basic network and security. I use FreeBSD since 4.5, FreeBSD-CURRENT on my laptop. I helped to reverse engineer and analyse the security of a voting computer in the Netherlands, and some art installations 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, a LISP dialect (dynamic, multiple inheritance, object-oriented), which even resulted in a TCP/IP implementation 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, an excellent book); a key event for me was the international conference on functional programming (ICFP). I wondered how a gradually typed 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. 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", where we mechanised proofs of the functional correctness of imperative code (PIs: Peter and Lars Birkedal). 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, 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, I also started (with David) the idris-mode for emacs. 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, a clean-slate operating system written in the high-level language OCaml. 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 project) with Peter Sewell. I primarily worked on TLS, MirageOS, opam signing, and network semantics. In 2018 I relocated back to Berlin and am working on robur.

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 and commercially 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), and the community is sufficiently large.

Me on the intertubes

You can find me on twitter and on GitHub.

The data of this blog is stored in a git repository.