From 4cfc3d4826036f586931ecebe9bdc1b92bfa691f Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Thu, 18 Jan 2018 15:58:10 +0100 Subject: [PATCH] typo, plus theorem prover -> proof assistant --- Home | 2 +- Technology | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Home b/Home index 2d75f94..161c1bd 100644 --- a/Home +++ b/Home @@ -17,7 +17,7 @@ With our approach to systems development we provide the following advantages for * minimal codebase without mutable state allows to reason about entire systems and adherence to specification * extensive library ecosystem, yet minimal trusted code base at runtime * rapid prototyping with a seamless path from prototype to production -* possibility to formally verify important parts with a therorem prover +* possibility to formally verify important parts with a proof assistant Our team is eager to develop applications for high assurance, which seamlessly diff --git a/Technology b/Technology index 2bb9c20..eff1e58 100644 --- a/Technology +++ b/Technology @@ -144,8 +144,8 @@ module interface. ### Verification -A large subset of the OCaml semantics has been -[mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover. +A large subset of the OCaml semantics has been [mechanically proven +sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a proof assistant. 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,