Axioms

Introduction

An axiom or postulate is a statement that is taken to be true (Wikipedia: Axiom). Without axioms, we couldn't have even the most basic laws. Every mathematical law has some axioms supporting it. When we talk about programming, this is no different.

In a programming language, an axiom is something that is preconstructed in the programming language, but can't be constructed (or it isn't worth constructing, usually for efficiency reasons) in such programming language.

If we go to the origins of Lisp, McCarthy's original "LISP 1.5 Programmer's Manual" constructed the full language with five functions: CAR, CDR, CONS, EQ, and ATOM. These five functions need to exist before we can construct Lisp. Which means, we can't construct them from the programming language, otherwise we would end in an irresoluble loop: prove the language can exist by constructing the five primitive functions, prove the five primitive functions by constructing them in the language.

The fix for this is introducing these five functions as axioms: we assume these functions exist, and we make them exist by _cheating_. In this context, cheating is using another programming language that already exists in order to construct the axioms in this new programming language. At this point you may ask: "Where this other programming come from?" In some sense, that's another axiom. We assume it exists, like C. Everyone uses C to bootstrap other programming languages. But if you don't want to assume C exists, you can go lower and construct C from Assembly. Which forces us one level deeper, and now we have to assume Assembly exists. But now we have to assume Assembly exists, but also we can construct it from machine code. Which forces us to assume machine code exists. Well, I can buy a microprocessor in a shop, and it understands machine code, so that's a (somewhat hacky) fix for it. The point is, the axioms of a programming language are always smaller than the programming language itself, which makes the problem of constructing the "original axioms" smaller and smaller, constructing lower and lower level axioms to prove more complex axioms, until the axioms we have to construct are so basic that we can easily prove them manually.

If you read up to this point and you are thinking that this is another Functional-Programming obsessed article (because I started talking about Lisp), you are totally wrong. This is about all the programming languages, regardless of paradigm, popularity and criticism. Let's run an example through a more popular programming language: Java.

An analysis of the axioms of Java

James Gosling, Mike Sheridan, and Patrick Naughton initiated the Java language project in June 1991.[26] Java was originally designed for interactive television, but it was too advanced for the digital cable television industry at the time.[27] The language was initially called Oak after an oak tree that stood outside Gosling's office. Later the project went by the name Green and was finally renamed Java, from Java coffee.[28] Gosling designed Java with a C/C++-style syntax that system and application programmers would find familiar.[29]

(https://en.wikipedia.org/wiki/Java_%28programming_language%29)

When Gosling, Sheridan and Naughton started working on Java, nothing existed that could execute Java. The JVM didn't exist. That's a problem if you are a Java programmer and you want your Java programs to actually run and be executed. So here is the first axiom (almost) every Java programmer in the world takes as granted:

Assuming there is a JVM, then my Java program will be able to run.

Then they summon the overlords at Oracle and ask them for a JVM.

But that's not the only axiom the Java programmers assume. There is another obvious one:

Assuming there is a Java compiler, then my Java source code can be converted to Java bytecode in the format the JVM will be able to run.

And again we summon Oracle to do the job.

The obvious extrapolation to other programming languages is:

Python programmers assume the Python interpreter has been implemented.
C# programmers assume the C# compiler and the CLR exists.
JavaScript programmers assume a browser capable of executing JavaScript exists. Alternatively, they assume the NodeJS virtual machine exists.

And so on.

Subtler axioms

But having a compiler, an interpreter and a virtual machine are not the only axioms we assume as programmers. There are many other, many of them subtler. Let me show you an example.

class HelloWorldApp {
    public static void main(String[] args) {
        System.out.println("Hello World!"); // Display the string.
    }
}

This is a "Hello World" in Java. The first example you learn in Java. The simplest program possible, other than the empty program. You want to see a magic trick? I'm going to make this program fail. Observe. Now it works:

root@7f367cb418c5:/# java HelloWorldApp
Hello World!

Now it fails.

root@7f367cb418c5:/# mkfifo fifo
root@7f367cb418c5:/# java Blah > fifo
_

See, it doesn't even complete executing. This "Hello World" is exactly the same as the previous one, but it can't complete it's execution. Why is that? The pipe has something to do with it. But what it is exactly?

Well, by piping to a fifo we broke one of these axioms we all programmers assume true. This axiom reads as follow:

There is this stdout file, which can receive arbitrary quantities of information, and displays such information on the console. And my program can write to it.

A pipe is a weird substitute for stdout. It works as long as someone on the other side is happy to read all the data that is being written. Which is something that I deliberately forgot in this case.

There are many more axioms we assume true, but are not necessarily true, such as:

There will be enough memory to load and run the system.
The operating system will be compatible with the application.
The hardware will be compatible with the application.
The libraries required by the application will be in place so the application can find them.
The system as a whole won't explode in the middle of running the application.

And many others.

Your own axioms

Ok, great. Lots of random axioms. All of them made by others. But how do I make my own axioms?

Well, theoretically, once you have enough axioms to make your system Turing-complete, theoretically the programming language can do as much as a computer can do. In practice, if allowed enough of the right resources. At this point, the mathematical problem of having a system strong enough to actually do anything becomes the engineering problem of having a system strong enough to be used in real-world situations with limited resources. Let's see how.

You introduce a new axiom in a programming language by modifying the compiler, usually to create a new primitive or a new function, or a new built-in. You write this extra functionality in another programming language, such as C, and somehow make the compiler for your language use it. This is something done so often that compiler designers decided to implement a standardized way to use it. They call it FFI: Foreign Function Interface. And each programming language has a version that is essentially similar to the others, but follows the specific details of the underlying language. The Java guys have Jep 191, the Python guys have ctypes, and so on.

But why would any Turing-complete programming language implement some of the possible constructions using FFI, I/E morally cheating the programming language? The usual reason is not theoretical, but engineering. No one doubts you can implement matrix multiplication in Python, probably using a bunch of for loops. What everyone doubts is that you can implement matrix multiplication in Python using the SIMD instructions of modern processors, using a cluster of GPUs, so you can train a neural network in a thousandth of the time (or less) that it would take your Python program.

So that's the reason why any programmer would want to introduce axioms into his favourite programming language: to make it more effective in his current situation.

Closing

Now you know a bit more about programming language theory, and why it matters on the real world. Now go and use this knowledge to make a better world!