--- title: About author: hannes tags: overview, myself, background --- ## What is a `full stack engineer`? Analysing the word literally, we should start with silicon and some electrons, maybe a soldering iron, and engineer everything all the way up to your favourite mail client. 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 trustworthyness 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 those projects, which cover topics on various layers above hardware. ### Myself I'm a [hacker](http://www.catb.org/jargon/html/H/hacker.html) (in the original sense of the word), 3X years old. 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). In my spare time, I'm not only a hacker, but also a barista. I like to travel and repair my recumbent bicycle. Fast forwarding a bit, I learned about the operating system Linux (starting with SUSE 6.4) and got hooked (using YaST, setting up basic networking (NFS/YP/Samba)). I joined the [Chaos Computer Club](https://www.ccc.de) around 2000. I learned a bit Perl, PHP, and also FreeBSD (I still use FreeBSD-CURRENT on my laptop). I helped with [analysing 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 setup the network (backbone, access layer, wireless, service (DHCP/DNS)), struggling with mainly Cisco hardware from their demo pool, but also some HP, Force10, Juniper equipment. In the early 200X I started to program a lot of [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/). I got really 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 for sure ICFP in 2005. I wondered how a [gradually typed](http://homes.soic.indiana.edu/jsiek/what-is-gradual-typing/) Dylan would look like. I spent some effort on that, leading to a master thesis, but the result was not too convincing (too slow, type system not sound). Additionally, Dylan has a small community, which has a hard time to maintain the self-hosted compiler and 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 started a PhD in a very ambitious research project "Tools and methods for scalable software verification" (mechanised proofs of the functional correctness of imperative code) with 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 artifacts 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 depedently 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 homogenous 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. ### Links 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/) in case you're interested. No comments here, but you can open issues on the [data repository on GitHub](https://github.com/hannesm/hannes.nqsb.io).