Do you think we could apply it for a large systems that which we know? Well, if it does not help, what is the alternative? Now, can we really test a correctness of the software? These are the formal matters, we can use a formal matters and could establish a correctness of the software.
It is a complicated process and tedious. In fact this also could be applied for a small situation and restricted environments. We may not be able to apply for a large system, and also the type of program which we require would be a very high program for this sort of a job. So, how do we test it?
The second problem is: when we say the formal specifications, can we really write, can we express ourselves formally the requirements, the user requirements? What is a the validity of these formal statements? So, basically we do not have really the methodologies to see that a formal software could be defined and can be proved as for correctness.