From 8b6966e5056175e11a2124f9f13e84171bef31d7 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Fri, 1 Apr 2016 20:21:28 +0200 Subject: [PATCH] initial --- Posts/About | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 107 insertions(+), 3 deletions(-) diff --git a/Posts/About b/Posts/About index 128a072..47b6f05 100644 --- a/Posts/About +++ b/Posts/About @@ -1,7 +1,111 @@ --- -title: About myself +title: About author: hannes -tags: overview, general +tags: overview, myself, background --- -This is just a test [](https://berlin.ccc.de/~hannes/ike0.png) \ No newline at end of file +![Sun](https://berlin.cc.de/~hannes/sun_e2016.png) + +## 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, 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. 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 both academically and commercially used, compiles to native code, has a +fast runtime, and the community is big enough that several people are working on +the compiler full-time. + +### 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).