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

typo, plus theorem prover -> proof assistant

Browse source
This commit is contained in:
Hannes Mehnert 2018-01-18 15:58:10 +01:00
parent 1bd9f4f3e7
commit 4cfc3d4826
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Home
View file

@ -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 * 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 * extensive library ecosystem, yet minimal trusted code base at runtime
* rapid prototyping with a seamless path from prototype to production * 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 Our team is eager to develop applications for high assurance, which seamlessly

4
Technology
View file

@ -144,8 +144,8 @@ module interface.
### Verification ### Verification
A large subset of the OCaml semantics has been A large subset of the OCaml semantics has been [mechanically proven
[mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover. sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a proof assistant.
OCaml is the implementation language of the well-known 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, [Coq](https://coq.inria.fr). Development in Coq can be extracted to OCaml code,