Why aren't we researching more towards compile time guarantees?

Question

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems to give stronger compile-time guarantees than any dynamic type system.

From what I understand, Ada goes even further with regards to compile time checking, and is able to detect a greater range of bugs ahead of execution. It's also considered fairly safe, given that, at some point in time, it was chosen for delicate fields (when programming errors may cost human lives).

Now, I wonder: if stronger static guarantees, leads to code that is more documented and safe, then why aren't we researching more in that direction?

An example of something that seems to be missing, would be a language that instead of defining a generic int type that has a range determined by the number of bits of the underlying architecture, one could have ranges (in the following example Int [a..b] describes an integer type between a and b included):

a : Int [1..24]
b : Int [1..12]
a + b : Int [2..36]
a - b : Int [-11..23]
b - a : Int [-23..11]

or (taking this from Ada):

a : Int [mod 24]
b : Int [mod 24]
a + b : Int [mod 24]

This language would select the best underlying type for the range and would perform compile time checking on the expressions. So that, for example, given:

a : Int [-3..24]
b : Int [3..10]

then:

a / b

will never be not defined.

This is just an example but I feel like there's a lot more that we can enforce at compile time. So, why there seems so little research on this? What are the technical terms that describe this idea (so that I can find more informations on this topic)? What are the limits?

Answer 1

I am not in a position to tell how much more research should be done on the topic, but I can tell you that there is research being done, for example the Verisoft XT program funded by the german government.

The concepts which I think you are looking for are called formal verification and contract based programming, where the latter is a programmer-friendly way of doing the first. In contract-based programming you first write your code as normal and then insert so called contracts into the code. A readily usable language which is based on this paradigm is Spec# by Microsoft Research, and the functionally similar but slightly less pretty Code Contracts extension for C# which you can both try out online (they also have similar tools for other languages, check out rise4fun). The "int with range type" you mentioned would by reflected by two contracts in a function:

Contract.Requires(-3 <= a && a <= 24);
Contract.Requires( 3 <= b && b <= 10);

If you want to call that function, you then have to use parameters which are ensured to meet these criteria, or you get a compile time error. The above are very simple contracts, you can insert almost any assumption or requirement about variables or exeptions and their relation which you might think of and the compiler will check if every requirement is covered by either an assumption or something that can be ensured, i.e. derived from the assumptions. That is why where the name stems from: The callee makes requirements, the caller ensures that these are met - like in a business contract.

Under the hood, code contracts are usually combined with knowledge about the inner workings (operational semantics) of the programming language into a list of verification conditions. This list represents basically one big logical proposition $P(x_1,x_2,...,x_n)$ with $n$ free variables - the inputs of your program. If the proposition $P$ is true for all possible variable assignments, then the program is considered correct. To check whether or not this is the case, an SMT Prover is used. From the CS side, those two are the critical parts of the process - the generation of verification conditions is tricky and SMT is an either NP-complete or undecidable problem, depending on the considered theories. There is even a competition for SMT solvers, so there certainly goes some research into this. Additionally, there are alternative approaches to using SMT for formal verification like state space enumeration, symbolic model checking, bounded model checking and many more which are also being researched, albeit SMT is, afaik, currently the most "modern" approach.

Regarding the limits of the general idea:

• As previously stated, proving the correctness of the program is a computationally hard problem, so it might be possible that the compile time check of a program with contracts (or another form of specification) takes really long or might be even impossible. Applying heuristics which work well most of the time is the best one can do about it.
• The more you specify about your program, the higher gets the probability of having bugs in the specification itself. This can lead to false positives (the compile time check fails even though everything is bug-free) or the false impression of being safe, even though your program still has bugs.
• Writing contracts or specifications is really tedious work and most programmers are too lazy to do it. Try writing a C# program with code contracts everywhere, after a while you will think "come on, is this really necessary?". That is why formal verification is typically just used for hardware design and safety critical systems, like software controlling airplanes or automotives.

One last thing worth mentioning which does not quite fit the above explanation is a field called "Implicit Complexity Theory", for example this paper. It aims at characterizing programing languages in which each program you can write falls into a specific complexity class, for example P. In such a language, each program you write is automatically "ensured" to be of polynomial runtime, which can be "checked" at compile time by simply compiling the program. I do not know of any practically usable results of this research, however, but I am also far from being an expert.