hannes/hannes.robur.coop
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

.

Browse source
This commit is contained in:
Hannes Mehnert 2016-04-03 13:15:58 +02:00
parent 3229b29a2a
commit 87ef293e88
1 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
Posts/About
View file

@ -2,6 +2,7 @@
title: About title: About
author: hannes author: hannes
tags: overview, myself, background tags: overview, myself, background
abstract: introduction (myself, this site)
--- ---
## What is a "full stack engineer"? ## What is a "full stack engineer"?
@ -37,7 +38,7 @@ first encountered programming in high school around 1995: Borland's Turbo Pascal
(which chased me for several years). (which chased me for several years).
Fast forwarding a bit, I learned about the operating system Linux (starting with 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 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). UNIX. In 2000 I joined the [Chaos Computer Club](https://www.ccc.de).
Over the years I learned various things, from Linux kernel modifications, 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 Perl, PHP, basic network and security. I also started to use [FreeBSD](https://www.FreeBSD.org) around 4.5, still using a FreeBSD-CURRENT
@ -59,16 +60,16 @@ I got excited about programming languages and type theory (thanks to
[types and programming languages](https://www.cis.upenn.edu/~bcpierce/tapl/), an [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 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/) [gradually typed](http://homes.soic.indiana.edu/jsiek/what-is-gradual-typing/)
Dylan would look like, leading to my master thesis, Dylan would look like, leading to my master thesis. Gradual typing is the idea to evolve untyped programs into types 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.
but the result was not too convincing (too slow, unsound type system). My 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 Another problem with Dylan is that the community is very small, without sufficient time and energy to maintain the
self-hosted compiler and IDE. self-hosted compiler(s) and the graphical IDE.
During my studies I met [Peter Sestoft](http://www.itu.dk/people/sestoft/). 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), 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 I did a PhD in the ambitious research project "[Tools and methods for
scalable software verification" (mechanised proofs of the functional correctness scalable software verification](https://itu.dk/research/tomeso/)", where we mechanised proofs of the functional correctness
of imperative code) with Peter and [Lars Birkedal](http://cs.au.dk/~birke/). 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 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, 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 several times refactored, and most of its shared mutable state was removed. The