For 50 years, the ability to code has been an intellectual and professional super-power. It’s a great deal of fun and has been a reliable path to interesting, high-impact, high-paying jobs, and in some cases even to extraordinary wealth and world-changing innovations. That said, I see a future in which programming as taught and practiced to date — what I will call mere programming — will no longer provide quite the same level of competitive advantage. By mere programming I mean writing code — typically in imperative programming languages such as Java, Python, C, C++, or Rust, or in functional languages such as Haskell or Scheme — possibly using “software engineering” tools and methods such as “agile development,” employing software testing as an approach to ensuring that code has no bugs that produce immediate functional failures, and then hoping for the best and depending on feedback from the use of the software to reveal additional problems that have to be addressed.
There are two reasons why mere programming of this kind seems destined to lose some of its shine. First, we are now seeing a dramatically increasing supply of people who are or who will become very good at it. This is the result of both spreading awareness of the benefits of having programming skills and of recent major success stories in computer science education. CS is now by far the most popular college major at many leading institutions. And there are now many vibrant efforts in the US and around the world to bring programming to younger children, in high school and even in elementary school. Second, mere programming is increasingly mismatched to rapidly growing of industry and government for code we can rely upon to run essentially all of the critical systems of our society: banking and finance, transportation and logistics, agriculture, healthcare, defense, and so forth.
It’s great that we’re teaching everyone one to code, but what we continue to teach is more akin to carpentry than to serious engineering. What’s missing in the teaching and practice of mere programming is the application of concepts, tools, and methods rooted in mathematical logical to formulate and to substantiate precise claims about critical engineering properties of the code that is being produced. We’re producing students who can write code but who generally lack even a basic understanding of how to analyze code using the kinds of rigorous methods that are widely employed in the engineering of physical systems. Instead, we are teaching and practicing the writing code, giving it some testing, then hoping for the best. and recovering when problems are discovered. The result is that we have built a civilization that increasingly rests of a sort of software swamp: solid enough for sunny days but at risk of catastrophic failures during future crises, including, in particular, failures caused by adversaries who have already exploited bugs in code to compromise it so that it can be made to fail on demand.
The problem with mere programming is that it is inherently incapable of producing code that is reliable, safe, and secure enough to rely on for one’s life and for the security of one’s nation. We now have overwhelming evidence showing that it’s practically impossible for human beings to get code right using only the methods of mere programming. These methods have been mostly okay for a long time because they are perfectly capable of producing nominally functional code, and because the risks posed by faulty software have been serious but have generally not risen to the level of existential threats. That has now changed. Our lives and the security of our nation now depend on the reliable functioning of software: for finance, transportation of of food and other goods, and so on. In the critical societal systems of the future, code that’s not assuredly right in specified dimensions is simply unacceptable, yet we continue to produce code using the same unreliable methods that we’ve been using for the last fifty years. What the world now needs are people who can not only code, but who understand the logic of software and how to apply concepts, tools, and methods based on it to produce code that comes with mathematical assurances of critical properties.
The “hot ticket” for the future, then, is in knowing not only how to code, but how to produce provably trustworthy code for critical applications. And that requires more than the knowledge of and skills of mere programming, of what one might call software carpentry. What it requires in addition to practical programming knowledge and skills is an understanding of the logic of software. The role of logic in software is akin to that of calculus in the engineering of physical systems: one simply cannot produce assuredly sound systems with it. The software super-power of the future is in knowing how bring logic and computing together to enable trustworthy specification, design, analysis, composition, certification, and evolution complex software and software-driven systems.
The carpentry analogy might help. Carpenters are skilled craftspeople who can build lovely homes. One cannot overestimate the value of skilled carpenters. We need them: a lot of them. But when one moves from building sheds, garages, and homes to building skyscrapers and urban centers carpentry skills are no longer remotely sufficient. When cities were built using only such skills, we ended up with cities of wood, and we saw the consequences in fires that literally destroyed whole cities. That is analogous to the state of software today. It’s working but its lack of vitally important engineering properties is putting the entire world at risk. In the realm of cities, the development and application of scientific and mathematical concepts, methods, and tools to specify, analyze, produce, and certify trustworthy buildings, and the dissemation of this kind to practitioners in the form of building codes, put an end to such catastrophes. Today, by analogy, we are producing many software carpenters but very, very few people equipped with sufficient knowledge and skills in the application of the analogous techniques needed to produce truly trustworthy software and software-driven systems.
My main educational aim at this time is to lay groundwork that will enable us to start to transform computer science education from a focus on producing mere software craftspeople to a focus on producing professionalswith the knowledge and skills needed to produce code that we can demonstrably rely upon for our most critical applications, which are now everywhere. To this end, my teaching in recent years has focused on bringing the emerging field known as proof engineering to students at both undergraduate and graduate levels. At the undergraduate level, I teach a CS1 course on programming using the pure functional programming language of a constructive logic proof assistant. In this course, students build the fundamental elements of practical programming languages and tools from the ground up, starting with the bare logic of a dependent type system. This approach is constructive in the sense that students are never asked to use something that they did not build themselves. No steps are skipped. The course concretely develops a core library of purely functional abstract data types, then builds a simple imperative language and its operational semantics on top of that library, and then finally explores how modern industrial languages, such as Python, implement these fundamental elements of programming. This course does not itself expose students to logical specification and analysis of programming, but it provides them with a deep understanding of the programming prerequisites needed immediately to move into the topic of rigorous logical specification, proof engineering, and production of mathematically certified code, which I believe should occur as early as their second semester of undergraduate computer science studies. This is a radical idea that has not been tried before. It is working, at least as far as CS1 is concerned. I have taught the course twice and now understand how to work out remaining areas of difficulty. This work has attracted the attention of senior investigators at Microsoft Research and I am now collaborating with several of them on this project. Similarly, at the graduate level, I teach proof engineering techniques supported by modern proof assistants, following a curriculum developed by Prof. Benjamin Pierce of the University of Pennsylvania. Brining such ideas to students at the beginning of their careers in programming requires exceptionally careful attention to issues of sequencing, explication, and exploration of concepts, programming mechanisms, and their applications. I’m now working on the second of a two-course introduction to computer science for students new to CS, one that will bring logic and proof engineering from the graduate level to the early undergraduate CS curriculum.
In the future, software engineers will deliver not just code but code accompanied by precise logical propositions asserting that their code has certain critical properties and by mechanically checked proofs that these propositions are actually true. One can then not only count on the code having the asserted properties; one can also use the assertions exported by given models to build proofs of proposition about larger systems into which given modules are integrated. The software modules of the future will deliver not only code but also logic. Recent work with my colleague, Prof. John Knight, extended these ideas to an include an interpretation of the mathematical logic, mapping its formal terms to real-world meanings, to complete the linkage of computational logic to real-world effects. If it all sounds hard or boring, especially for beginners, it’s not. It’s beautiful material that students appreciate and that has proven accessible to students with no prior experience in computer science.
I have just launched a bare web site, LearnFunctionalProgramming, where I will present the undergraduate CS1 course. I will be populating that site in the weeks and months to come. I will then develop a second site, LearnProofEngineering, where I will present a second undergraduate course on logical specification, reasoning, and certification of trustworthy code. I explain these ideas in some more detail on a separate page, about Why Mere Programming is No Longer Good Enough. This material is still evolving. Feel free to contact me for more information.