From 37e0ff0453b96b29f41951dcff7b4e33ef070ed2 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Sun, 17 Sep 2017 00:20:16 +0100 Subject: [PATCH] . --- Technology | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/Technology b/Technology index 4911471..2c2e94c 100644 --- a/Technology +++ b/Technology @@ -139,19 +139,29 @@ 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. -### Semantics and security +### Verification -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. +A large subset of the OCaml semantics has been +[mechanized](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover, and +this metatheory is verified. -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. +OCaml is the implementation language of the well-known proof assistant +[Coq](https://coq.inria.fr). Development in Coq can be extracted to OCaml code, +as demonstrated by [compcert](http://compcert.inria.fr/), a formally verified +optimizing C compiler, in order to be compiled and executed. The other +direction is also possible: OCaml code can be translated into Coq definitions +(using [Coq of OCaml](https://github.com/clarus/coq-of-ocaml/)). + +The National Cybersecurity Agency of France reviewed the implementation of the +OCaml runtime system, [their +report](http://www.ssi.gouv.fr/agence/publication/lafosec-securite-et-langages-fonctionnels/) +altered some language modifications, such as that strings are no longer mutable. ### Modern dialects and compile targets 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/)). +simcorp, lexifi) and academia. In 2016, Facebook developed [reason](https://reasonml.github.io/), a dialect of OCaml which syntax is closer to JavaScript, and easier to comprehend for