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.