robur/homepage-data
4
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

.

Browse source
This commit is contained in:
Hannes Mehnert 2017-09-17 00:20:16 +01:00
parent 7154bcd65f
commit 37e0ff0453
1 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
Technology
View file

@ -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