A Better Model of Computation

Modern software engineering is based on problematic fundamentals.

One thing I loved about computers when I was young, was their deterministic nature. If you understood their rules, you could perfectly predict what they would do. However, as the complexity of computers and software has grown, they increasingly behave in practically non-deterministic ways. Programs often crash or suddenly run out of memory, or hang, or get really slow for no apparent reason.

Some of this in unavoidable, since complexity is the enemy of practical predictability. But we could be doing much, much better than how we are now.

Computer programs have side effects that we care deeply about, such as memory use, CPU time utilization and even heat generation. But if you ask a programmer how much resources their program uses, you'll be lucky if they can give you even the vaguest of answers. We measure all these effects at a top level, and hope that our benchmark runs are representative of real world use. What we should be doing, is using the computer to measure these things from the bottom up.

What we should have, is a world where we know exactly how long a computer program will take to execute down to the nanosecond, given specific inputs.

But wait, doesn't that involve solving the halting problem?

Yes, but only if we're using Turing complete languages. That's why we need to abandon Turing completeness as our foundation paradigm.

To illustrate my perspective, we can segregate the Turing Machine model into two parts, a terminating pure function taking a state and returning a state, and a simple fixed-point combinator for feeding the pure function into itself. The fixed-point combinator is trivial and not worth talking about; all the interesting logic lives in the terminating part.

The pure functional programming community has been working on many such segregations of deterministic and non-deterministic code already. The FRP model (if you get past the continuous time part, which distracts from my main point) shows that we can use a state machine to bridge the IO behavior of a computer and the pure functions that actually define what we care about in software. It's a small jump from there, to eliminating non-terminating pure functions entirely.

Of course, perfect deterministic behavior relies on an open hardware model, which unfortunately is not the case in our current world. It would take the compiler having a perfect model of the CPU it was compiling for, with all its caches, branch prediction and instruction prefetch circuitry modeled in software. But even without that, the terminating paradigm should allow compilers to give us bounding predictions that are much more detailed than current big omega metrics.

So if this model of computation is truly better, how to go about demonstrating it?

My plan is to develop a simply typed lambda calculus, marry it to an FRP framework, and write a simple game like tic-tac-toe in it. After that, I want to add in refinement typing and work it into the FRP framework so that inputs that would violate preconditions are not allowed rather than generate runtime errors.

There is much more I could talk about, such as implications for operating system design, opportunities for optimization and how to transpile existing languages into a terminating model, but I'll wait until I have a working proof-of-concept to write about what comes next.