Given the US govt. security agencies recommendations for using Memory Safe Languages (as if there is more than one!), let’s bootstrap the right understanding of what the “memory safety” means from the first principles.
The “first principles” will be indeed the first ones, because we will go all the way back to the underlying recurring patterns in What Is, from which the fundamental mathematical notions have been captured, properly generalized, abstracted away, named and their properties systematically studied.
There is a minimal (which means nothing can be removed) abstract mathematical formalism to define (and study the properties of) any [possible] commutable [mathematical] function, and composition (nesting) of such functions – The Lambda Calculus of Alonzo Church.
Most of the texts on the Internet would claim that it has “just three things” (three kinds of terms in the grammar):
- [lambda] abstraction
- application [of lambdas]
- [immutable] bindings [of values to variables]
This is a gross oversimplification, which ignores the important subtleties. These “bindings” and “abstractions” (and the results of “applications”) does not exist “in a vacuum”. There is a universal notion of an “Environment”, which is a global lookup-table (or even a pure function!) that can be conceptualized as a set of ordered pairs – the symbols (names) being associated with (bound to) corresponding values. These bindings are immutable. New ones can be added to the “table”, producing a new, updated “table” (or a pure function!).
Whether the symbol (a name) is already in the “Environment” or not is irrelevant, since nothing is ever “destructively updated or over-written”, the only possible operation on an environment is to extend it with a new binding (new information), and to produce a new (updated) environment. Some would argue that this is the simplest but proper abstract model of a whole Universe on which the Causality Principle is acting upon.
These abstract notions are not arbitrary or specific to The Lambda Calculus formalism. The notions of “shadowing” (of bindings), which are just an immediate consequences of how the environment is, of “bound and free variables”, and of so-called “lexical scooping”. The last two ones rely on the fact that environment is not a single “flat” set of ordered pairs (implemented or represented as an ordered sequence, since there is no other way – to write anything down as a sequence implies to have some particular order), but in addition to have the notion of nested “frames” of the environment, which conceptually are just “smaller environments” within (not dissimilar of the organelles within a living cells, which used to be particular kinds of cells nested withing other cells).
Each lambda abstraction has its own implicit tiny [nested] “environment” (its own frame of environment, as they call it), which has only one binding (of its own [single] parameter).
Again, nothing here is arbitrary or “invented” – everything has been “discovered” by well-trained mathematicians (as the way to have a minimal and correct representation of universal notions). These notions are applicable to any system of formal logic, starting from the Gerhard Ghentzen’s “Natural Deduction”, and everything based on it, etc. The symbol \(\Gamma\) in the traditional notation denotes an “environment” which contain all the previously derived results and the axioms (to begin with). This is not a random coincidence. Our minds have something similar, implemented in “synaptic states within a particular network of neurons”.
Such kind of “structural formalism”, more precisely defined, is used to study the semantics of programming languages in general. The “raw computer memory” is being modeled as a higher-level (higher than a merely array of “machine words”) as a bunch of “cells”, which are, again, just another specialization of a set of ordered pairs.
There is, however, a principal difference – in all such formal mathematical models the contents of a “memory cells” can be destructively updated or over-written, with an irrecoverable loss of the previous content (information loss). At least in theory, it does not have to be that way – mathematically, the memory can be extended with new cells that “shadows” the previous ones, so when we look up a value the most recent one will be the answer. The problem is that this idealistic model requires an infinite storage, which is just impossible. The enlightening realization, however, is that mutation is not required or even necessary in principle. Molecular structures which are being used in molecular biology are “supposed by Evolution” be this immutable.
Okay, biology of Life is way more complicated than our grossly oversimplified models of it, but there are the underlying principles which can be discovered, understood and relied upon. For instance, each “small” molecule is a perfect copy of one another (due to the various electro-chemical constraints), so [each] one is as good an the other. This is exactly how our “immutable values” shall be.
These “basic building blocks” of molecular biology [once being used] do not supposed to change behind its back (when it does, due to the increase of an entropy and external factors, this is a decay, “loss of an intended function”, disease and disintegration (death).
So, having a lot of immutable identical copies (or clones) is “the discovered by Evolution itself way to do it”. “Immutability” is not a fancy ivory-tower academic’s intellectual masturbation (as degens on /g/
usually put it), this is a universal principle, at least for this particular Universe as it is.
Notice that changes in (mutations of) particular molecular structures actually do occur withing the living cells “all the time”, especially in the so-called ATP pathways, but they are done by (within, inside of) particular highly specialized and unique “embedded” (withing a cell) molecular structures called “enzymes”, which at least in theory, are not dissimilar to our “pure functions”. One could say that the universal notion of a pure function (which embody a particular transformation from particular inputs to particular outputs), is a properly captured and generalized (actually, the most general) notion of what a biological enzyme is (among other things). It is as general as to capture a “single distinct step of causality itself”.
Lets return back to Earth for a while. What all this “proper philosophy” has to do with Rust? Well, after struggling with abominations like C++ Evolutionary processes “discovered” that by [accidentally, after trying and failing with literally everything else] basing a language on the truly universal notions would eventually yield a more ordered and stable “structure”, just exactly as it was within molecular biology of Life Itself.
No, it is not the case that the original designers of Rust were geniuses. It is just that there is no other way – everything has to converge back to What Is and to its universal notions, which are discovered, not invented.
The only way of doing computations (and programming) just right, is to base it on the universal underlying notion of a directed acyclic graph (or a DAG), which partially captures the Causality Itself (in a particular locality). The great FP guys of the past have intuitively discovered this fact, by having their terms to form a DAG (what else could it be?) and to discover the graph-reduction method of evaluation (reduction) of such DAGs.
Rust is light-years away from being a near-perfect pure language like Haskell, but at least attempts has been made to build it on actually proper foundations and principles.
Just as the Simple Typed Lambda Calculus (an evolutionary step toward better stability) restricted and formalized the way too-general notion of applicability of anything to anything else, by introducing a type-discipline (which restricts what can be applied to what by a set of explicit rules), Rust is trying to restrict the imperative “chaos” with a way more strict type-discipline (a particular set of complementing each other rules) to what can and cannot be done at the semantic level.
The formalized notions of “move semantics”, “ownership”, “lifetimes” and, in particular, the formalized and enforced at the compile time restrictions on use of “references” is an evolutionary step in the right direction (of more stable intermediate building blocks). Again, it is not “genius insights”, it is mere evolutionary processes (which select “local optimums” of simplicity and stability) at work.
Everything in Rust can be understood from these principles. The main one is that “restriction, or very careful selection of what to use, is the only way”. This is exactly how Life Itself came to be – by selecting very restricted by the given environmental constraints stable intermediate forms, drooping (eventually discarding) what is not stable-enough.
So, the takeaway is this – as an evolutionary step of a procedural imperative language, Rust has been built upon way better, less random theoretical foundation than any other imperative language in existence, approaching the mathematical ideal of pure functional languages.
In the next chapters we will build it from the ground up using the universal notions of nesting, “enzymes”, duck-typing (which is how molecular structures are “typed”) and what not.