6. Conclusion
Proof assistants such as Coq make it possible to produce safe software despite its complexity. Clearly, not every program needs to be formally verified, but the number of applications that need to be safe justifies the emergence of a profession we can call proof engineering, which requires skills in both logic and software engineering.
Among the various proof assistants, Coq stands out for its reliability, extensive standard library, and a large number of interactive proof tactics.
Its complexity might frighten off the novice user, but it's not Coq that's too complicated, but the rigorous proof, particularly of algorithms and programs, which requires sufficiently comprehensive tools.
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
Conclusion
Article included in this offer
"Software technologies and System architectures"
(
230 articles
)
Updated and enriched with articles validated by our scientific committees
A set of exclusive tools to complement the resources
Bibliography
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page. http://www.ocaml.org/...
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
