commit ee4b5f95ab2f2c186f9e1a95ee0b36cb48b8fa68 Author: Victor Maia Date: Sun Sep 4 19:12:08 2022 -0300 Kindelia Manifesto diff --git a/README.md b/README.md new file mode 100644 index 0000000..11a4cbd --- /dev/null +++ b/README.md @@ -0,0 +1,91 @@ +The Kindelia Manifesto +====================== + +What is the true nature of computation? A hundred years ago, humanity answered that very question, twice. In 1936, Alan +invented the Turing Machine, which, highly inspired by the mechanical trend of the 20th century, distillated the common +components of early computers into a single universal machine that, despite its simplicity, was capable of performing +every computation conceivable. From simple numerical calculations to entire operating systems, this small machine could +do anything. Thanks to its elegance and simplicity, the Turing Machine became the most popular model of computation, and +served as the main inspiration behind every modern processor and programming language. C, Fortran, Java, Python are +languages based on a procedural mindset, which is highly inspired by Turing's invention. + +Yet, the Turing Machine wasn't the only model of computation that humanity invented. Albeit a less known history, also +in 1936, and in a completely independent way, Alonzo Church invented the Lambda Calculus, which distillated the common +components - not of machines, but of different branches of math - into a single universal language that was capable of +modeling every mathematical theory. What was surprising, though, is that this language, unexpectedly, could also perform +computations. The same algorithms that could be computed by Turing Machines procedurally, could also be computed by the +Lambda Calculus, through symbolic manipulations. The idea of using the Lambda Calculus for computations inspired the +creation of an entire new branch of programming, which we call the functional paradigm. Haskell, Clojure, Elixir, Agda +are languages based on the functional mindset, which is highly inspired by Church's invention. + +If both Turing Machines (and procedural languages), and the Lambda Calculus (and functional languages), are capable of +computation, which mindset is the "right one"? When it comes to raw capabilities, neither. Still on the 20th century, it +was proven that, when it comes to computability, Turing Machines and the Lambda Calculus are equivalent. Every problem +that one can solve, can also be solved by the other. That insight is known as the Church-Turing thesis, which +essentially states that computers are capable of emulating each-other. If that was completely true, then the choice +wouldn't matter. After all, if, for example, every programming language is capable of solving the same set of problems, +then what is the point in making a choice? + +Yet, the Church-Turing hypothesis makes a statement about computability, it says nothing about computation. In other +words, a model can be inherently less efficient than other. Historically, procedural languages such as C and Fortran, +have have consistently outperformed the fastest functional languages, such as Haskell and Ocaml. Yet, languages like +Haskell and Agda provide abstractions that make entire classes of bugs unrepresentable. Historically, the functional +paradigm has been more secure. + +The Turing Machine and the Lambda Calculus aren't the only models of computation worth noting, though. In 1983, Stephen +Wolfram introduced the Rule 110, an elementary cellular automaton that has been shown to be as capable as both. Wolfram +argues that this system is of fundamental importance, and that a new kind of science should emerge from its study. +These claims were met with harsh scepticism; after all, if all models are equivalent, what is the point? Yet, we've just +stablished that, while equal in capacity, different models result in different practical outcomes. Perhaps there isn't a +new branch of science to emerge from the study of alternative models of computation, but what about the design of +processors and programming languages? + +A model of computation has a significant impact on the way we design our languages, and several of their drawbacks can +be traced down to limitations of the underlying model. For example, the parallel primitives of the procedural paradigm, +mutexes and atomics, provide a contrived, complex solution to multi-threaded synchronization. As a result, parallelism +is generally considered hard, and programmers still write sequential code by default. Similarly, security isn't natural +to the procedural paradigm. Global state, mutable arrays and loops generate an explosion of possible execution paths, +edge cases and off-by-one errors that make absolute security all but impossible. Even highly audited code, such as +OpenSSL, is often compromised by out-of-bounds exploits. The functional paradigm handles both issues much better: there +is an enourmous amount of inherent parallelism to be extracted from pure functional programs, and logic-based type +systems make entire classes of bugs unrepresentable. But if that is the case, then why functional programs are still +mostly single-threaded, and bug-ridden? And why isn't the functional paradigm more prevalent? + +The culprit, we argue, is the underlying model. As much as the Turing Machine, and, thus, the procedural paradigm as a +whole, is inadequate for parallelism and security, the Lambda Calculus, and the functional paradigm as a whole, is +inadequate for real-world computations. The fundamental operation of the Lambda Calculus, substitution, may trigger an +unbounded amount of copies of an unboundedly large argument. Because of that, it can not be performed in a bounded +amount of steps, and, thus, there isn't a physical mapping of substitution to real-world physical processes. In other +words, substitution isn't an atomic operation, which prevents us from creating efficient functional processors and +runtimes. Attempts to solve the issue only pushed it into other directions, such as the need of shared references, which +inhibit parallelism, or garbage collection, which isn't atomic. The failure of the functional paradigm to achieve +compatible efficiency impacted its popularity, which, in turn, lead to tools like formal verification to never catch up. + +This raises the question: is there a model of computation which, like Turing Machine, has a clear physical +implementation, yet, like the Lambda Calculus, has a robust logical interpretation? In 1997, Yves Lafont proposed a new +alternative, the Interaction Combinators, on which substitution is broken down into 2 fundamental laws: commutation, +which creates and copies information, and annihilation, which observes and destroys information. In a sense, this may +resemble SKI combinators, but that isn't a good analogy, since SKI combinators still include non-atomic operations: K +may erase an unboundedly large structure, and S may copy an unboundedly large structure. The charm, and elegance, of the +Interaction Combinators is that its reduction laws are truly atomic: each operation can be completed in a constant +amount of steps, and has a clear physical mapping. Not only that, they're inherently parallel, in the same sense that +the Lambda Calculus has been claimed to be, in theory, but without the issues that let it to be, in practice. + +Interestingly, every aspect which is considered good in other models of computation is present on Interaction +Combinators, while negative aspects are completely absent. Like the Turing Machine, there is a very clear physical +implementation. Like the Lambda Calculus, there is a robust logical interpretation which is well-suited for high order +abstractions, strong types, formal verification and so on. Curiously, both the Lambda Calculus and the Turing Machine +can be emulated by a small Interaction Combinator, with no loss of performance, while the opposite isn't true. This +suggests that, while the 3 systems are equivalent in terms of computability, the Interaction Combinators are more +capable in terms of computation. Under certain point of view, one could argue that both the Turing Machine and the +Lambda Calculus are slight distortions of this fundamental model, with a touch of human creativity, caused by our +historical intuitions regarding machines and mathematics, which is the source of their inefficiencies. Perhaps machines +and substitutions aren't as fundamental as we think, and some alien civilization has developed all its mathematical +theories and computers based on annihilation and commutation, with no references to the Lambda Calculus, or the Turing +Machine. + +We, at the Kindelia Foundation, hold the view that Interaction Combinators are a more fundamental model of computation, +and, consequently, that computers, processors and programming languages inspired by them would offer tangible benefits +compared to the ones we built based on Turing Machines and the Lambda Calculus. The Kindelia Foundation was created to +research this new model of computation, and, through the different mindset it brings, catch insights that will let us +produce groundbreaking technology that will push humanity towards the next level of computational maturity.