From 7cfd9db75e499776e4d6a8594ccfcc74984b1a1c Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Tue, 12 Apr 2016 08:19:27 +0100 Subject: [PATCH] . --- Posts/OperatingSystem | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Posts/OperatingSystem b/Posts/OperatingSystem index 9da17de..7281e97 100644 --- a/Posts/OperatingSystem +++ b/Posts/OperatingSystem @@ -87,6 +87,8 @@ Being without funding back then, we didn't get far (hugest success was a Dylan), and as mentioned earlier I went into formal methods and mechanised proofs of full functional correctness properties. +### MirageOS + At the end of 2013, David pointed me to [MirageOS](https://mirage.io), an operating system developed from scratch in the functional and statically typed language [OCaml](https://ocaml.org). I've not @@ -169,7 +171,7 @@ The OCaml runtime was reviewed by the French [Agence nationale de la sécurité leading to some changes, such as separation of immutable strings (`String`) from mutable byte vectors (`Bytes`). The attack surface is still big enough: logical issues, resource management, and there is no access -control. This is fine for this website, publishing of content is "protected" by relying on GitHub's +control. This website does not need access control, publishing of content is protected by relying on GitHub's access control. I hope I gave some insight into what the purpose of an operating systems is, and