.

Technology

@@ -140,26 +140,27 @@ unikernel, the TCP/IP stack natively implemented in OCaml is being used.
 A MirageOS developer does not need to reason about compilation targets, just about the
 module interface.
 
-### Security reviews
+### Semantics and security
 
-TODO: OCaml runtime vom franz. BSI reviewed, solo5 noch kein wirkliches review
+Parts of the semantics of the OCaml language have been
+[formalized](http://www.cl.cam.ac.uk/~so294/ocaml/) and its soundness has been
+proven in a mechanized way.
+
+The OCaml runtime system has been reviewed regarding its security by the National Cybersecurity Agency of France, the [report](http://www.ssi.gouv.fr/agence/publication/lafosec-securite-et-langages-fonctionnels/) influenced some language changes, one of them is that strings are no longer mutable.
 
 ### Modern dialects and compile targets
 
-OCaml is known as a mature programming language that is used in both
-industry (facebook for compilers, jane street for trading, docker, ahrefs,
-simcorp, lexifi) and academia (coq, compcert).
+OCaml is a mature programming language that is used both in
+industry (Facebook, Jane Street Capital, Docker, ahrefs,
+simcorp, lexifi) and academia (the [Coq proof assistant](https://coq.inria.fr/), the formally verified optimizing C compiler [compcert](http://compcert.inria.fr/)).
 
 In 2016, Facebook developed [reason](https://reasonml.github.io/), a dialect of
 OCaml which syntax is closer to JavaScript, and easier to comprehend for
 beginners.  Reason and OCaml code can be easily combined in a single
 application, since the same compiler is used.
 
-Links:
-- [OCaml for the masses](http://queue.acm.org/detail.cfm?id=2038036)
-- [Why OCaml (from realworldocaml)](https://realworldocaml.org/v1/en/html/prologue.html)
-- [Replacing Python with OCaml in 0install](http://roscidus.com/blog/blog/2013/06/09/choosing-a-python-replacement-for-0install/)
-- [Why tezos uses OCaml](https://www.tezos.com/static/papers/position_paper.pdf)
+More literature on why OCaml is a good choice in the modern world has been
+written by Yaron Minsky (Jane Street) in the article [OCaml for the masses](http://queue.acm.org/detail.cfm?id=2038036), and more recently by the crypto-ledger [tezos](https://www.tezos.com/static/papers/position_paper.pdf).
 
 ## Current state and future directions