Program checking

Abstract

In languages such as Pascal, the programmer can arrange to have the compiler check such things as the range of the value of a variable only by defining a new type or sub-type. I have investigated how more powerful checking facilities might be provided if they were divorced from the type machinery, and also if the necessary language constructs were designed independent of what any particular compiler would check at compile-time.