Towards Provably Correct System Synthesis and Extension

Our ultimate goal is to define a framework and a methodology which will allow users to construct or extend complex reasoning systems in such a way that the correctness of the resulting system is guaranteed. Our approach is based on the following principles: (i) construct the prover according to certain general (but precise) criteria, in particular maintain a sharp distinction among the logical, control, and interaction components; (ii) use a uniform framework to specify these three levels; (iii) represent (selected parts of) the code in a classical first order theory, use the inference capabilities of the system to reason deductively about this theory, and, as a result, synthesize new code which can be pushed back in the underlying implementation. This paper describes the approach, what we have done so far and how we intend to proceed to pursue our ultimate goa