Values amount to timeless abstractions for which the concepts of updating, sharing and instantiation have no meaning. … Objects exist in time and, hence, can be created, destroyed, copied, shared and updated.
This understanding is more relevant to the modeling of the material world, which contains things that exist in time. I think it also suggests that mutability implies lifecycle and subsequently implies the modeling of the material world as a paradigm.
I asked attendees about their experience with this understanding. The students told me they never learned it. The teachers told me they were not teaching it to undergrads. There must be something missing here.
There’s so many of these beautiful ideas that collapse upon hitting the world in which we live. The paper makes these assumptions over and over again, that we can create and destroy things, “just like in the material world”, unfortunately it comes crashing head-on to the the first law of thermodynamics, which states explicitly that we can’t, do just exactly that, creating and destroying things.
The cost exists in the material world, as it exists in the memory in which our programs live. Some people have explored this connection extensively, that connection between resourced based computation and logic. Lafont, for example, and understanding the subtleties of the following two words is important:
The fundamental laws of computation are commutation and annihilation.
If we’re taking the material world as a paradigm, there’s something really interesting that we can look at, linear logic(!), which lives at the core of optimal lambda reduction and seems to coexist with the rules of the natural world. I think there’s definitely a point to be made about looking at how the material world works, and what computation model best maps to that reality.
At least, we might wan to search for something that doesn’t goes straight against the first law of thermodynamics.
Hot take: One thing I could say about the creation and destruction of resources and computation. I think variables/arguments/bindings/clojures are a mistake, they should not exist at all in computation, and if I had to make a prediction, one day, they won’t. Accessing things by name is fundamentally flawed as a resource management mathematics, because it’s based on traditional logic which obfuscates resource consumption and duplication.
FILE * f = new File();
f.destroy()
f.append('c') // error
Names allow to cross the boundary into a world in which things can be accessed, instantiated or destroyed without being aware of the cost, or simply accessed after they have stopped existing, and this distance from how the world in which we live works might be an indication as to why it’s computationally inefficient and error prone. I think the reason why this whole paradigm(as opposed to another without bindings, like tacit programing) leads to needless amount of errors from operating on things that don’t exist, is that same distance.
Anyways, object instantiation/sharing/as-values is a nice idea, one that I’d classify as Mathematically elegant, thermodynamically fictional.
The new object is allocated space so that it is independent from existing objects. As a part of its metaphysics, space allocation is enforced by the runtime.
Compare this to nominal type systems[1], where types are distinguished by their names and not their structures.
Since things cannot be simply created or destroyed, my understanding is that you intend to describe systems that do not exchange matter with the outside. Which means the boundary of the system must be established to use your modeling language.
Is my understanding correct?
This is what I first think of, because my goal is to construct some kind of language for cognition, and we are not born knowing any such boundaries.
Why do we need object-orientation, apart from what has already been discussed on this forum? Object-orientation provides facilities for identity throughout a lifecycle. The identity of a mutable variable is the variable, or its left value, written down explicitly and statically. The identity of an object is an automatically created name at run time. These names only have the operation of equality (and maybe copying). Crucially, both names and left values only make sense when there is mutability. Otherwise, they are called “bindings”.
Sometimes, we do not need this kind of identity. If we describe a physical system (at least, a classical one), and want to identify something in it, this should simply involve some kind of boundary drawing. After this, we know everything that is inside the boundary, because we are already working with a model. It might make sense to assign some kind of name to these boundaries within physical systems. Then, we track each object throughout the lifecycle. Unless already existing, a boundary can only be created with 0 volume, and be destroyed when it has 0 volume. But we do have to allocate these names, and this shouldn’t be called a violation of thermodynamics. What may be considered a violation of thermodynamics must already be the case before drawing boundaries.
We can only draw boundaries when we already have a model. Somewhat naively, consider the following view of a physical system state:
which in extract_properties hides a lot of physical information and also uses a lot of physical information more than once. It is not apparent how some conservation in the physical system maps to some conservation in the domain-specific state. When writing object-oriented code, I think people really just want the domain-specific view to work, without writing the full model, and it gets incorrect really quick.
So, here is how I imagine a linear, thermodynamics-conforming language will be used in this situation.
The full model, including its updating algorithm, is written in this language.
The boundary recognition and domain-specific view are constructed with a normal language. It can access the full model without restrictions and allocate any amount of space.
The view is view-only; input through the view is undefined.
It may be argued that this object-oriented model is an illusion, a convenient but leaky abstraction that is often mistaken for the world itself. Do “things” actually exist? Does their “identity” have any basis in physical reality?
Gottfried Leibniz’s Principle of the identity of indiscernibles states that two things are identical if and only if they share the same and only the same properties.
It seems to me that “identity” only exists in an abstract ideal space where we disregard time or any change in the state of an object, or its surroundings (!) since no object exists by itself separate from its environment. In reality everything is changing, nothing is the same, and a “thing” is not even identical to itself in the next moment.
An interesting aspect of linear logic, which I’ve been studying for a while since the discussion on concatenative languages started, is that it makes you question the value of names, and therefore variables and functions. How they’re commonly assumed as being fundamental to computation and the practice of programming.
A name is a kind of GOTO statement that implicitly breaks linearity and locality. What’s curious is how this relates to the resource-based view of quantum information, where the act of observation (such as referencing a variable) is a stateful effect that “consumes” the value as a resource.
Vaughan Pratt. Linear logic for generalized quantum mechanics, in Proceedings of Workshop on Physics and Computation (PhysComp’92). http://boole.stanford.edu/pub/ql.pdf
Peng Fu, Kohei Kishida, Peter Selinger. Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (July 2020). doi:10.1145/3373718.3394765, pdf, video
Modern quantum programming languages integrate quantum resources and classical control. .. The “no-cloning” property of quantum mechanics means that quantum resources are linear in the sense that one cannot duplicate a quantum state. This is why linear types have been adopted to provide a type theory for quantum computing.
It’s a deep subject where most of the material is over my head, but I’m finding a way to understand some of it by reading tons of primary sources. I’m acquiring a kind of “taste”, an aesthetic preference for the style of thinking and areas of investigation I enjoy, and a common thread involves “thinking visually”. Imagine my joy on learning there’s a relationship between logic and topology (spaces).
This approach models “the material world, which contains things that exist in time” as a flow of values through computational process and logical/topological operations.
In this view there is no “thing” separate from the process, no object with its own state and methods. It shows why object-oriented programming is typically full of self and this. Having deconstructed objects, there is no longer a need for names, to maintain an identity over time, and it eliminates the mismatch between an object’s state (its model of self and world) and the world itself.
An interesting angle is compiling programs into hardware (“hardware compilation”).
In proof theory, the Geometry of Interaction model was introduced by Jean-Yves Girard shortly after his work on linear logic. It has been applied to deep compiler optimisation for lambda calculi. A bounded version of it named the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits.
Hardware compilation of programming languages via game semantics is a natural approach based on solid foundational results.
In hardware, type systems must be realised as compositional protocols. ..Because the circuits are a direct representation of the semantics of the type system and the language, a compiler can be constructed denotationally.
Function application is simply circuit composition, contraction is implemented by AMs [a special circuit called an activation manager] of the right type, and lambda abstraction is, through the currying isomorphism, only a relabelling of ports.
It opens up a wealth of questions by considering what’s necessary to compile a program or function into hardware such as digital circuits.
For example, what is the cost of accessing the value of a variable? How can a language take advantage of the inherently parallel nature of circuits? Why is there such a mismatch between conventioal programming paradigms, even LISP, and the hardware necessary to implement and run them directly?
Trying to “bridge the gap” doesn’t seem enough, I think, and it might be better to reconceptualize how to do programming from the ground up (again) based on mathematical logic and the material world, at least space-and-time, as it is without the layers of abstraction we’ve taken for granted.
Leibniz is easily applied to the identity of timeless values. Leibniz identity usually means right-value equality. (I have not really seen left-hand Leibniz proposed by anyone.)
You can state object identity in the Leibniz fashion, but it does not make sense to combine left-hand and right-hand equality when there is mutation, hinting at a fundamental disagreement between Leibniz equality and mutability.
As described before, I think a kind of boundary drawing is involved. This boundary drawing is subjective.
If you have a full model and then draw boundaries, the exposed read-only DSL appears to be more expressive than what you can get by modeling the same thing object-first. This may correspond to the problems of abstraction you pointed out.
Are you suggesting that @neauoire’s thermodynamically-based language be compiled to specific hardware, taking advantage of the thermodynamic properties?
About hardware compilation of programs, I was suggesting it more as a “lens” or metaphor, as a way to think about paradigms like object orientation, functional reactive, or concatenative programming.
If you were to write programs as if you were designing an electrical circuit, or as if the compilation target of your language is hardware (not on hardware but implementing the algorithms in hardware) - what priorities and concerns would arise, how would it differ from conventional approaches where, for example, you can create and destroy objects as if it cost nothing. Or how would you prove the correctness of a program before you “burn” it on to hardware and deploy it, since changing it after that is more costly or impractical.
It’s also, for me, a way to think about the physical nature of computation without the abstractions typically associated with it like objects, variables, and functions which can be constructed from simpler primitives that are “closer to the metal”. The metal being actual hardware, or mathematical logic that is metal-like or crystalline (eternal or long-lasting truths that can be proven) compared to programming on top of layers of software, like living organisms (temporary ever-changing states).
I’ve often wondered about this, because I grew up reading circuit diagrams as a kid before I got into 8-bit programming, and always missed the sense of clarity that were in circuits. (Though feedback loops in circuits always confused me, and still do).
First, we’d have much more of a focus on parallelism rather than “sequential execution”. We’d have something like a dataflow or reactive model.
Second, instead of “calling functions” or “running subroutines” (let’s assume that jump/goto is just “call followed immediately by return”), with an assumption of near-zero cost for a function call, we’d instead be a bit more aware that every time we “call” (more precisely, “at every place we call”), we are creating a full copy of (instantiating) a function-like-object, including all of its calls/instantiations. There’d probably be a compilation-like stage that does a bit of analysis and tries to allocate hardware efficiently.
Not sure if it would be easy to have a very compilation-light, point-free, programming model like Forth on this sort of setup. There might well be one, but it would probably be about networks and signal flows, not about stacks or about term-rewriting. Perhaps there’d be maybe a few standard numbers of local inputs/outputs (four or eight perhaps, or two inputs and two outputs, if we’re looking at a 2D grid of cells) and we’d reference those instead of “top x elements of stack”.
Third, instead of loops we’d probably have blocks of operations/modules that keep a little bit of state (like a chip does) and receive and emit a time-varying stream of signals. That’d be the most efficient usage of hardware. We’d want to keep modules running for as long as possible because the startup/copy/build cost would be high. We’d also care quite a lot about the locality of signals in a way that we sort of don’t in the fetch-instructions-and-data-from-RAM model (though we should already care about locality much more than we do, because of the number of levels of caching we now have, extending from the CPU cache all the way to CDNs on the Internet). Our function-like-modules would also be a bit object-like if they’re keeping some local state. As indeed chips on a circuit board are.
Fourth, recursive loops really wouldn’t be very easily possible (except as time-varying signal streams). They could be done but each level of recursion inside a module (so like, left-recursion instead of right-recursion) would need more hardware allocated to it, so it would always be thought of as an “expensive” option.
The LLM AI people seem to work in a world much like this with GPUs, with Python “tensor” libraries managing essentially the “compilation to silicon” part. The big attraction of the “attention” model was that it didn’t require recursion, so it could be spammed out onto vast amounts of parallel silicon (consuming vast amounts of electricity as a result).
When it comes to designing multiprocessing systems and networks (whether physical or virtual cloud setups), we also start to become much more like “hardware”. There’s time and space cost of bringing up / deploying “processes”, “servers” or “containers”. We very much don’t have a good way to think about this level, though, and we certainly don’t have any “languages” that let us describe the parallel data flows even on a single machine let alone a network. We just have glorified “config files” to wrangle for all our cloud architectures, and a few sketchy network diagrams that don’t have any precise meaning and are really just internal marketing copy.
It would be awesome if we could write / design / conceptualise in one language which was fundamentally parallel and hardware/network-like, and then have that language run / compile-to / be-deployed-on anything from silicon or GPU, to a local machine, to a private or public network or cloud. Then we wouldn’t have to deal with a massive impedence gap and a re-architecting / rewriting problem when we jump scale (with all the errors that introduces), and it also might be a way to avoid lock-in problems of proprietary cloud services. If we can state clearly and precisely what the exact shape of our computational network should be, then it’s much harder for a big megacorp to jump in and say “no no no, you want our proprietary opaque network blob (and NSA intercept feed) in the middle there”.
Edit: And before someone jumps in with the old argument of “but you can’t have one language that does everything! Use the best tool for the job! Keep switching up your languages all the time!” I want to pre-empt that and say: on the contrary, I assert that we can indeed, if we choose to, have a single modelling language that describes different systems that we want to wire together, for the purposes of simulation and analysis and certification before we deploy. Human languages work this way: we don’t have hard barriers between them, we just keep adding concepts to them. If I want to talk about, say, Relativity, I don’t have to switch from English to German just because that was Einstein’s first language and therefore there are some concepts that “just can’t be expressed in English, and shouldn’t be, use the right language for the job”. That’s silly. Translation exists, and words can be borrowed! Concepts can indeed be exported out of and imported into a language, and if they couldn’t be, no communication between humans speaking different languages could ever exist! Further, in English (or any other human language), I can describe the internal operation of German as a language, down to the grammar, and the same the other way. Our human languages have introspection and reflection, to put it in software terms.
We might not want a single unified software package distributed across the Internet. Though we still might need that in situations where it’s very difficult to ship core binary OS/VM updates: if, for example, we wanted to bake an extensible language into the ROM firmware of something like a game console or a home wireless router, and we only got one shot at distributing that console/router before the planet’s lights went out and a world war started. Or if every revision to a shipped binary required separate approval from the EU or from Google - a dystopian state that we’re rapidly starting to head towards. In these two cases, we’d really like that VM/OS that we ship, that we only get one or a very few shots at upgrading, to be both extremely secure and extremely extensible. And it would be worth spending a few thought cycles thinking about how we might create something that could survive a return to a 1970s like environment where OS/VM patching is very hard, rather than relying on “ship the OS/VM/firmware broken and patch it every week lol”. What if the global trusted patching infrastructure goes down one day - or is subverted by an authoritarian/fascist government? As it looks like it might? Can we at least launch one rowboat from our Titanic that gets ahead of that iceberg?
But it must be logically possible for a single modelling language to express, within itself, linkages between a whole stack of systems, so that we could, eg, run top-to-bottom efficiency and security checks on the system-of-systems as a whole. And so it might be a small step forward if we can sketch out at least one possible candidate for such a language as an existence proof. A double step forward if that modelling language could also function somewhat efficiently, or at least not stupidly inefficiently, as an implementation language, rather than just being limited to modelling (as, say, logical proof assistants are right now).
And by “language”, I really here only mean “grammar”, with the assumption that almost all the details of that language can be shunted off to libraries, sets of nouns and verbs etc. But at the moment we don’t even really have a decent grammar for such a dataflow/network-state description language - despite most of our modern software systems being sprawling, stateful parallel networks rather than sets of linear instructions followed in order. Our modern software systems are also full of dangerous security bugs, precisely because we’re not rigorously modelling and analyzing them before we deploy them. We do use “type systems”, which are sorta kinda like the type of parallel/network modelling language I envisage, but even the best of those still don’t do enough of the modelling and analysis work that we desperately need to do.
Formal languages are not the same as human languages. Communication between humans depends on a shared context, which serves to disambiguate and fill in missing details. Formal languages must express self-sufficient systems, in all relevant detail.
The promise of LLMs is to model the linguistic context and thus allow us to communicate with machines as we do with humans. Which works well enough at some kind of collective level, but not for individuals or small groups. The LLM’s context is the average context of the people who contributed to the training material. When you ask ChatGPT for medical advice, it responds for the average person that expresses your symptoms. When you ask your doctor, you get advice based on your medical history, your physical environment, the expression on your face, and a lot more.
Very much agreed there. LLMs aren’t a great path forward in my opinion, especially for highly complex machinery that has to work, and it worries me that so much of software engineering is rushing to try to rebuild itself on such a flaky foundation. Let alone trying to replace humans with it, which is even worse.
I’m thinking more about something like proof assistants, but trying to find a way to make those much simpler and easier for actual humans to code in directly. Like Prolog, which I keep circling around, because although it isn’t quite right, it managed to capture such a sweet spot of a simple, efficient, declarative-like syntax and semantics that is also reasonably easy for humans to understand how the machine will parse it.
That’s one of my big problem with LLMs. It’s pretty much impossible to understand/predict how a model will respond to any given piece of input. How can we competently manage a machine if we can’t build a mental model of what the machine is doing?
Instead of giant, centralized, opaque, statistical models, I want small, local, transparent and deterministic mini-machines that can be plugged together like Lego blocks. I used to think that Object Oriented Programming had solved this back in the 1990s (that’s what they all taught us in school, through into the early 2000s)… but then it turned out that it’s actually really hard to plug different OOP systems together, much more so than it ought to be, so that our OSes still aren’t really based on an object model, though an OOP style of programming is used inside various subsystems. This annoys me, since in the 1980s everyone was promising “object oriented OSes coming next year” and then it just didn’t happen. But maybe it didn’t happen because OOP was very ill-defined.
Even without a unifying OOP modelling language, we can still use an OOP kind of concept to picture how the Internet works. Systems send messages to each other, update their state in response, etc. This sort of works, but it doesn’t quite give us enough precision to make guarantees about how subsystems will operate beyond just “receive/send message that matches a certain shape/type, and in between lol whoops anything can happen”. It would be nice to be able to describe and enforce hard guarantees about the behaviour of a subsystem and its relations to its subsystems, and not just have methods be opaque Turing-complete blobs which can’t be easily analyzed.
Dataflow/reactive still maybe doesn’t solve this modelling problem, but it gives a slightly different (functional/declarative) perspective that I think might be useful.
I’m beginning to think that, as one poster here mentioned a few months back, probably all of the useful parts of the reactive paradigm can be captured by adding just one construct to pure functional programming: “previous value of (variable name)”, defaulting to a system standard “unbound” value - nil/null/false/zero etc. I don’t know for sure that that’s the case, but I hope it might be.
The “previous(x)” construct is very easy to map onto a hardware circuit diagram, which is one reason I like it - it’s essentially just a “delay loop” (maybe with a gate/latch/comparator circuit if we want it to represent discrete value changes, which we probably do) added to a local wire. I think every other kind of memory/state in digital circuits is built out of delay loops and comparators.
I don’t know how that construct might work in a point-free functional programming system without variable names, though. (Like SKI calculus as opposed to Lambda calculus). Kind of the whole point of reactive is that there exist “signals” or “channels” which have identity and values that can change, making them a bit object-like. Those entities might be able to not have names (like Prolog “unknowns”, or OOP objects), but they do have to have identity so that a downstream consumer can find them, connect to them and receive a stream of values. But perhaps in a principled, pure reactive system, every value would also be a signal, so “previous” on any value could maybe fetch its last one. (Being implemented, perhaps, in a minimalist Forth-like compiler as a quick count of instances of “previous” inside a word, with a local variable allocated for each instance, for each callsite ). Or, perhaps, on each word invocation (which might be easier for the runtime to track than values). Some values still might need to be “object identifiers” or “cell addresses”, as they are in Smalltalk, Forth or in Lisp (the difference being that Smalltalk identifiers and Lisp cell addresses are unforgeable, which is a very useful security/integrity property).
KL-1, the “Kernel Language One” of the 1980s Japanese Fifth-Generation Computer project - a parallel Prolog - had a slightly similar concept where it turned all its “unknowns” into signals/channels.
Something has an identity if it preserves its own dynamics, meaning that it changes but eventually it preserves some of its dynamics while maintaining some forms of freedom.
It so happens to be the same definition that biologists use to define life. It is that, the closure to constrains, closure to efficient causation.
This identity is a characteristic of the processes of a system, thus it is not a static notion of identity.
In my opinion, this is the correct definition of what an object should be, and not what we currently use.
Regarding linear logic and hardware programming languages, I would say that it is not the correct abstraction when we talk about networks.
Networks are nondeterministic, linear logic is deterministic.
So linear logic is good for logical circuits , but not for interactive distributed programs.
A language of independent autonomous processes / systems needs to deal with this nondeterminancy, to model it.
(‘I have spent too much time trying to understand linear logic only to find that it doesn’t fit the model. If I am wrong, please enlighten me’)
Edit :
By the way, functional réactive programming is also circuit like. That is my opinion.
I would say that the more shared context there is, the less able to have independent changes of modules / interactive programs.
This is the reason I went for theorem provers, each group can independently update its system. I do not try to solve a correctness problem. I am trying to solve a communication problem.
I understand why people are confused about using a theorem prover in this setting, but the problem is that they have wrongly identified theorem provers as a tool for provable correctness, and I don’t use it this way.
Oh I just noticed, @Apostolis it was from your post that I learned about Tangible Functional Programming. Thanks for that, I like the concept and since then have been studying the author’s work, following the path of research. I resonate with the line of thinking and subjects he’s engaged in, for example:
Why might one care about interpreting lambda expressions in terms of cartesian closed categories (CCCs)..? I got interested because I’ve been thinking about how to compile Haskell programs to “circuits”, both the standard static kind and more dynamic variants. Since Haskell is a typed lambda calculus, if we can formulate circuits as a CCC, we’ll have our Haskell-to-circuit compiler.
My hunch is that combinatory logic and linear logic are relevant to this question.
Maybe a network can be considered a large-scale circuit with asynchronous signals and processes. I imagine software design can learn more from how existing hardware systems solve the question of entropy, uncertainty, unreliability - building a (more) deterministic and predictable system with strategies like fault tolerance, error correction, exception handling.
Here’s a recent talk by the same author.
A Galilean revolution for computing: Unboundedly scalable reliability and efficiency. Video, Slides
It’s about how the current practice of programming and software development has created a big mess, and how formal logic, correctness, proofs, and mathematics can provide the solid foundation for a better approach.
Haskell, Rust, Lean.. From these I’m fond of Haskell, and slowly learning to read Rust because it’s practical and popular. I’m curious about Rocq and Agda too, since some of the researchers I’m interested in are using them to communicate their ideas.
In Galileo’s time, professors of philosophy and theology—the subjects were inseparable—produced grand discourses on the nature of reality, the structure of the universe, and the way the world works, all based on sophisticated metaphysical arguments.
Meanwhile, Galileo measured how fast balls roll down inclined planes. How mundane! But the learned discourses, while grand, were vague. Galileo’s investigations were clear and precise. The old metaphysics never progressed, while Galileo’s work bore abundant, and at length spectacular, fruit. Galileo too cared about the big questions, but he realized that getting genuine answers requires patience and humility before the facts.
– Frank Wilczek, The Lightness of Being: Mass, Ether, and the Unification of Forces
