March 19, 2014.
I’m developing a programming language that has a built-in automated theorem prover (rather than a traditional type system). My inspiration comes from Coq, an interactive theorem prover, and Whiley, one of the most intriguing programming languages I’ve ever seen.
Let me tell you a little about it. It uses a cool formal system called the sequent calculus (check out this amazing interactive tutorial from my fellow MIT colleague if you’ve never heard of it) and another system called Hoare logic. But that’s not important. The punchline is that all of the following are within the realm of possibilities:
- A type system for “free”. For example, in order to add two numbers, you must first prove that they are numbers (because that is the precondition for addition). Sounds annoying? This is where the “automated” part of “automated theorem proving” comes in. It works like a type inferencer—most of the time, the compiler can automatically prove that you’re doing a valid operation.
- Types that represent arbitrary mathematical predicates. Examples: the type of even integers, the type of sorted lists, or the type of non-singular matrices. These are called dependent types in my circle of friends, or, more specifically, refinement types.
- Guaranteed safety. You want to divide two numbers? You must prove that the divisor will never be zero. Except most of the time the compiler will prove it for you. No segfaults, no runtime checks, no nonsense.
- What about when the compiler can’t find a proof? No problem, just give it a high-level proof outline. It will try to fill in the details.
- Memory safety. The language will be garbage-collected (as is common in modern programming languages), but sometimes you want a little bit more control. You can manually allocate memory, but you must prove to the compiler that you free it later. No memory leaks allowed.
- Provable totality. You can prove that a function terminates—no accidental infinite loops. Or, if you like, prove that a function runs in \( O(n \log n) \) time.
- Prove arbitrary theorems. Every once in a while, an engineer might need to do this—and it’s nice to have the proof machine-checked.
- Concurrency. Prove that you have the only reference to a variable, and don’t worry about other threads mutating it. Or, in the face of shared memory, prove that deadlock cannot occur. (This is related to my Masters research.)
- Performance. Prove that you never access an array out-of-bounds, and then you don’t need an expensive runtime check on every array access.
- Security. Prove the absence of CSRF attacks. Or prove that a user can only access his/her own data (i.e., a static version of another MIT colleague’s work).
- Better collaboration. If a coworker breaks your code, the proof-checker will reject it and he/she will not be able to check it in.
It’s the ultimate in static typing. Of course these are ambitious ideas and I certainly panegyrized them a bit (in particular, automated theorem provers are typically quite dumb), but I could imagine a future in which all programming languages have a fancy proof system like this—especially if the programmer does not need to think about it most of the time. Wouldn’t that be neat?