From e624c3f0f8d8f0b9a2f9b91d7a4b0221195ea7e2 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Sun, 17 Sep 2017 00:03:34 +0100 Subject: [PATCH] . --- Technology | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Technology b/Technology index 1583ba2..6333778 100644 --- a/Technology +++ b/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