diff --git a/Posts/About b/Posts/About
index 9786636..dba5d92 100644
--- a/Posts/About
+++ b/Posts/About
@@ -2,6 +2,7 @@
 title: About
 author: hannes
 tags: overview, myself, background
+abstract: introduction (myself, this site)
 ---
 
 ## 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).
 
 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).
 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
@@ -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
 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.
+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.
+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](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/).
+I did a PhD in the ambitious research project "[Tools and methods for
+scalable software verification](https://itu.dk/research/tomeso/)", where we mechanised proofs of the functional correctness
+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
 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