|Computational class||Turing complete|
The author of Island believes that this is the computational model of the future and that in the year of 2100 all programming languages will use this computational model (if the human civilization survives for that long).
In this computational model, we first specify some basic logic (for example higher-order logic) and then we specify axioms (for example Zermelo-Fraenkel set theory), and finally the axiom of global choice.
We write programs by using the global choice to construct objects that satisfy a given specification. The interpreter uses some advanced AI to prove that there exists a model for that specification, so that the specification holds for the constructed objects. The interpreter then performs computation by proving things about the constructed objects.
We can construct natural numbers in the following way:
- Let be some ordered 3-tuple, where and are sets and is a function from sets to sets, such that
The interpreter proves that there exists a model for that specification, creates objects , and , and proves that all of the conditions hold for them. Then we can define addition of natural numbers in the following way:
- Let be some binary operation on sets such that
We define comparison of natural numbers:
- Let () be some binary relation on sets such that
We can define real numbers like this:
- Let be some 4-tuple such that
- is a totally ordered set
- is a field
- If is a non-empty subset of , and if has an upper bound (under ), then has a least upper bound , such that for every upper bound of ,
- (this requires some additional technical conditions)
Of course, we would first need to define what a field and totally ordered set are. This is just to demonstrate the point of how "defining" things would look like.
We can, for example, define number as the ratio between the area and the radius of the unit circle (we would need to define -algebra and Lebesgue measure first). We can then define what n-th digit of a real number means and we can "evaluate" number to any number of decimal places, just by letting the interpreter determine each of the digits of interest by proving/disproving that the digit is equal to some value. We do not need to bother about optimizations or advanced and complex algorithms. We simply specify what we need and the interpreter figures out everything for us.
The interpreter is able to prove any provable statement (provable within the system of axioms we specified).
There are some languages such as Coq or Lean that have the concept of "computation", but they are very limited in that regard. First, not all functions in them are computable. Second, their computation has only one "path" that can be followed.
The computation in Island is much more powerful. All functions are potentially computable and the interpreter can do whatever it wants to "compute" the result by proving/disproving statements about the result, eventually reducing the result to a single concrete value.
For example, we can create a 3D rendering engine that has infinite precision. We define the world, objects, light, reflections, mirrors, shadows, and so on. Then we let the interpreter render each frame by "computing" the RGB value of each pixel, by proving/disproving for each pixel that the specific color value of that pixel is less than or greater than some constant, eventually bisecting the value to an 8-bit integer and displaying it on the screen.