Correctness proof and design of language

Observing how Egyptians were practicing it, the Greek called it the measurement of land, or geometry. Generally, we only use geometrical measurements, and leave the notion of derivation to the followers of Pythagoras and Euclid. But the point is that geometry has two aspects, measurement and derivation.

The most successful measurement theory for software development has been the complexity of algorithms. On the other hand, derivation has not found a footing yet. The possibility of any form of success in the direction of derivation has been diminishing. The likelihood that a Riemann will make some geometry applicable to software correctness proof is moot.

Perhaps, we should seek correctness proof in an entirely different form. For instance, in manufacturing a car, engineers use various areas of science to demonstrate that each portion that they are dealing with is correctly designed. However, the actual car is assembled from all those parts, and the gluing material. The only correctness proof for the final product is a test drive. That just seems so dissatisfying for software.

It is more likely that the design of language and the roles of compiler and linker will eventually get us closer to a more satisfying mechanism for correctness proof. For instance, structured programming helps write programs that are closer to the way we think. On the other hand, type checking helps avoid sending incorrect objects to functions. The point is that, it is better to focus on the design of language for correctness proof rather than try to come up with a logic that can prove the correctness of programs in arbitrary languages.

Obviously, an engineer unfamiliar with the semantics of the language’s constructs and the intent of its linguistic facilities will not be able to make much sense out of a large number of error messages. The more sophisticated the language, the longer it takes to truly appreciate its facilities for correctness proof, and the proper interpretation of the error messages in correcting the code. Simply removing errors and warnings is not a justifiable development practice.

Regardless of the level of sophistication of a language, there will be areas that compiler and linker, or any other tool for that matter will not be able to help in detecting obscure errors. This is why a systematic final test drive (as for a car) is necessary.

Considering the degree of difficulty in mastering a language the question is, which language do we start with? In other articles I have argued that we should follow an evolutionary path, starting with C, C++ and now Z++. Starting with an entirely new language is like forcing a conquered nation to speak the invader’s language. Furthermore, C and C++ have stood the test of time.

Z++ is freely available from ZHMicro.