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

update

Browse source
This commit is contained in:
Hannes Mehnert 2018-01-04 14:48:41 +01:00
parent cb04d2f980
commit d9fe669c10
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
About
View file

@ -59,7 +59,7 @@ 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. 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. Dylan would look like, leading to my master thesis. Gradual typing is the idea to evolve untyped programs into typed 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). 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 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. self-hosted compiler(s) and the graphical IDE.
@ -92,6 +92,8 @@ clean-slate operating system written in the high-level language [OCaml](https://
hooked pretty fast, after some experience with LISP machines I imagined a modern hooked pretty fast, after some experience with LISP machines I imagined a modern
OS written in a single functional programming language. OS written in a single functional programming language.
From summer 2014 until end of 2017 I worked as a postdoctoral researcher at University of Cambridge (in the [rigorous engineering of mainstream systems](https://www.cl.cam.ac.uk/~pes20/rems) project) with [Peter Sewell](https://www.cl.cam.ac.uk/~pes20/). I primarily worked on TLS, MirageOS, opam signing, and network semantics. In 2018 I relocated back to Berlin and am working on [robur](http://robur.io).
MirageOS had various bits and pieces into place, including infrastructure for 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. 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 No access control, no secure sockets layer, nothing. This will be the topic of