112 lines
6.2 KiB
Text
112 lines
6.2 KiB
Text
---
|
|
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 my projects roughly on a weekly basis, 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. 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 (YaST, setting up basic networking (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 also started to use [FreeBSD](https://www.FreeBSD.org) around 4.5, still using a FreeBSD-CURRENT
|
|
on my laptop (unfortunately no Broadwell graphics). 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,
|
|
but the result was not too convincing (too slow, unsound type system).
|
|
Dylan suffers from a too tiny 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 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
|
|
GitHub](https://github.com/hannesm/hannes.nqsb.io).
|