The search for correctness has been a long-standing problem for, first of all, mathematics and then computer science. In computer science there is a very strong need for reliable information technology. And we need correct programmes. We need programmes that meet their specifications. This can be achieved only through strong methodologies that should be applied at any level of the software design cycle. First of all, we need specification languages in which to specify the behaviour of programmes. Then we want to derive from these specifications - in a top-down way - the programmes that meet the specifications. Finally we want to prove that the programme itself meets its specifications. We must say that only partial success has been achieved in the last few years and mainly in hardware design. The fact is that making specification and proofs is difficult because it requires ingenuity. But it should also be noted that while making proofs is difficult, checking them is not. So, we may think to have a system, a computer programmes, that interacts with the user in order to build a proof but then it checks the correctness of that proof in a completely automatic way.

---