We continue exploring the development of the relationship between computation, logic and algebra through primary sources.
We explore the development of the relationship between computation, logic and algebra through primary sources.
We learn how to encapsulate and compose TLA+ specifications, of the precise mathematical definition of abstraction, and compare TLA+‘s notion of abstraction with those of other formalisms. Plus some various cool stuff.
The post is here.
TLA, the Temporal Logic of Actions is the core of TLA+. It is a temporal logic that minimizes the use of temporal reasoning in favor of more ordinary mathematics. It is a general mathematical framework for describing and reasoning about algorithms and systems.
The post is here.
We explore the “data logic” of TLA+, the means by which TLA+ specifications describe a state of computation: its data structures. To do that, we first cover the basics of mathematical logic.
The post is here
TLA+ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.
The post is here
A certain tweet caught my eye this past week. I will not link to it because I don’t want to single out its author, who expresses an opinion which is rather common in some crowds, but it said: “Do the people behind the big mainstream languages not follow PLT at all?” What prompted this condescending remark was a Microsoft blog post about the programming language C#, which claimed the language is “state of the art”. Even though C# — like other mainstream languages — does use the best current tools for software development, that still seems to fall short in the eyes of the tweet’s author, who expresses a view I’d like to call theory supremacy, which is the belief that the study of theory, in this case programming language theory, directly implies the study of practice. Implied in this ideology is the belief that one can easily extrapolate from advances in theory to advances in practice. Theory supremacists are usually enthusiasts rather than researchers, and their belief is based on a misunderstanding of what it is that theory teaches us.
The study of theory is crucial and may certainly lead to — probably required for — eventual advances in the state-of-the-art, but the transition is neither obvious nor simple. This is especially true when the theory in question is programming language theory, particularly its sub-discipline concerned with designing programming languages, which studies the inherent properties of specific programming languages (as opposed to studying the semantics of arbitrary programming languages). There is no scientific principle that extrapolates from an inherent property of a system to a general “goodness” value, the latter being an empirical claim. The only scientific practice for establishing empirical claims is empirical observation.
To demonstrate that programming language design theory cannot yield the “best” programming language when disconnected from empirical study, let’s draw on the time-honored scientific tradition of considering the world around us. The most elaborate computational system known to us is life. Few computer scientists — even programming theorists — would deny that life is a computational system of the utmost importance. While it’s true that it is very different from most man-made software systems and cannot be compared directly to software because its goals, or requirements, are different, there is no doubt that life achieves its requirements rather well (although those requirements may not align with those of specific organisms, like ourselves), and that it achieves them employing many of the concepts studied by programming theorists. By mere observation, it is obvious that life has mastered concepts like abstraction (it can represent abstractions such as “leg” or “eye”), modularity and composition (cells, organs, symbiosis), maintainability and even meta-programming (chromosomal crossover, epigenetics, brains). Life also has no problem employing parallelism for efficiency, or handling concurrency.
The good news is, then, that abstraction and composition arise naturally, and may hint at the fact that those programming concepts may somehow be intrinsically tied to computation (see my previous post for a discussion about the difference between the two). This certainly opens the door to a programming-theoretic study of computation, something that programming theorists seem to intuitively believe can and should be done, yet have so far been unable to satisfactorily express1. The bad news for theory supremacists, and what they should find infuriating, is that the programming language chosen by life, at least here on earth, is not ML or Haskell, nor is it, as some would believe, Lisp. It wasn’t even hacked together in Perl, but written in the even messier, redundancy-filled language of nucleotides. My knowledge of molecular biology is dismal, but I doubt that DNA is really just, say, ML with a different syntax, or any other “state of the art” PL formalism. Protein interactions are such that it is doubtful that DNA has a convenient compositional semantics with respect to the phenotype (which is what matters), although an approximate compositional semantics may exist. Put simply and somewhat simplistically, life achieves all the programming goals the theorists say are good, yet it does it while taking a different route.
The reason for this heretical, infuriating choice for the most impressive computational system known is simple: the value of a programming language does not lie with inherent elements of the language, but with an interaction between the elements of the language and the properties of the programmer, which, in life’s case, happens to be natural selection (and possibly other forces). Since the mathematics of programming languages does not model the qualities of the programmer, it cannot possibly yield the best practical programming language by the power of theory alone. It can study the properties of specific kinds of abstraction and composition but not judge whether or not they are better in practice. Claims of superiority on scientific, rather than aesthetic, grounds must be based on the study of the nature of the programmer. Do people best think of programs as functions? As state machines? As queries and transactions? As a prioritized set of rules? Perhaps in a different way depending on the domain? One thing is certain: If you’re not interested in asking this question and others like it, you cannot define the state of the art for practical programming language design. Those who are interested in such questions — and people at Microsoft certainly are — are in a better position to do so.
The practical success of some ideas studied by programming theorists is no evidence in favor of theory supremacy. It is simply because theorists are drawn to constructions that are likely to be of service to human programmers just by virtue of the theorists being human themselves. This is the same reason for the practical success of ideas put forward by more intuitive language designers, whose work is explicitly motivated by more artistic, aesthetic ideals, and does not make claims to theoretical superiority.
1. Perhaps because in order to do that, the theory must encompass the program-programmer interaction, or the nature of the programmer as the computational collaborator that I mentioned in my last post. This may not be as far-fetched as it may sound, as useful information could perhaps be gained with simple complexity measures on the communication between the language and the collaborator.