search

objectionary / ideas

Here we keep ideas for future research in EO programming language and Polystat static analyzer
https://www.eolang.org
7 stars 0 forks source link

Offer tool support for formal proofs #28

Open andredidier opened 3 years ago

andredidier commented 3 years ago

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.

yegor256 commented 3 years ago

@andredidier what exactly do you suggest us to add to EOLANG?

Graur commented 1 year ago

@yegor256 Can we move it to https://github.com/objectionary/ideas/issues ?