In order to organise the complex system such as a proof interface, a modular design was chosen. The aim is to achieve a resulting system with simple interactions between modules, thus reducing the global complexity in the system. Eric S. Raymond explains this idea in his book [49], referring to the Rule of Modularity: ``The only way to write complex software that won't fall on its face is to build it out of simple modules connected by well-defined interfaces, so that most problems are local and you can have some hope of fixing or optimizing a part without breaking the whole.''
We agree with this summation, and after selecting programming libraries and languages with work with, we select a proof assistant capable of fitting into this style in §4.2. The rest of this chapter is then aimed at describing how these modules fit together (§4.3, System Architecture) and then what each module does internally.
|
|
|