Offer tool support for formal proofs

[andredidier]

In some domains, like critical systems (that involve loss of lives or loss huge amounts of money if something goes wrong) and security (where someone tries to exploit bugs in the software) it is paramount to have not only tests in place, but also formal proofs for system properties. As those proofs are usually long and complex, tool support is needed to handle them semi-automatically (people design the proof and a tool verifies its correctness). Example tools are Coq and Isabelle/HOL. The semantics of an EO program could be given in the Unifying Theories of Programming - UTP.