No programmers in five years?

A few weeks ago Emad Mostaque, the founder and CEO of Stability AI, made a bold prediction about the future of programming. He told the audience at Goldman Sachs 2023 Disruptive Technology Symposium that programming will cease to exist in five years.

“This is a much bigger disruption than the pandemic,” he told the audience, going back to his point about AI large language models successfully writing software code. OpenAI’s ChatGPT can pass Google’s exam for a high-level software engineer, Mostaque said, even though it’s a non-specialized model. “There’s no programmers in five years,” he predicted.

https://www.goldmansachs.com/insights/pages/stability-ai-ceo-says-ai-will-prove-more-disruptive-than-the-pandemic.html

While he does have a point that the profession will be completely disrupted and a lot of what programmers do today will be automated, I don't think that the profession will cease to exist entirely. The invention of high-level languages didn't displace assembly programmers, they still exist because there are still some tasks for which one needs to write assembly directly. Similarly, I think there will be things that language models can't do alone and will require input from a human programmer. If nothing else, we will still need programmers to double-check the outputs of language models. A language model can make mistakes, and it can be tampered with by bad actors, so we will still need some programmers to guard against that.

GPT4 designs a language

But that got me thinking, the language in which the language models will write its programs will need to make it easy to verify whether it is correct, and make it hard for mistakes to be introduced. It probably will not look like the languages most people use today. So I asked GPT4 to tell me what such a language would look like, the requirements, what languages are similar to it, and to design the beginnings of this language and give me some examples. Here is what it told me:

Language requirements

First, I asked GPT4 how would such a language look like:

Me: If we wanted to design a programming language that is completely provable and error-free so that it can be written by a language model but verified by a human and proven correct by formal verification systems, how is a language like that likely to look like?

GPT4: Designing a programming language that is completely provable and error-free is a challenging task. However, we can outline some key features that such a language might possess. This language would be designed with formal verification, simplicity, and readability in mind, in order to facilitate human verification and automated proof systems. Here are some features that could be part of such a language:

1. Strong typing: The language would have a strong static type system, which helps catch many errors at compile-time. Types could be enriched with additional information to express invariants and other properties, allowing for more precise verification.

2. Formal semantics: The language would have well-defined, formal semantics to ensure that the behavior of programs can be rigorously reasoned about. This would make it easier for formal verification systems to prove the correctness of the code.

3. Built-in support for contracts and specifications: The language could incorporate support for specifying preconditions, postconditions, and invariants directly in the code. This would help to express the intended behavior of the code and facilitate its verification.

4. Limited side effects and immutability: To simplify reasoning about program behavior, the language could minimize side effects and promote the use of immutable data structures. This would reduce the potential for errors due to unexpected interactions between different parts of the code.

5. Concurrency control: The language could provide constructs for managing concurrency that are amenable to formal verification. This might include using message-passing concurrency or other mechanisms that avoid shared mutable state, which is often the source of hard-to-find concurrency bugs.

6. Modularity and encapsulation: The language should promote modularity and encapsulation, allowing for the separation of concerns and the ability to reason about smaller parts of the code in isolation. This would make it easier to verify the correctness of individual components.

7. Simplicity and readability: The syntax and constructs of the language should be designed with simplicity and readability in mind. This would make it easier for humans to review and understand the code, helping to ensure its correctness.

8. Standard library and tooling: The language should come with a verified standard library that provides commonly used data structures and algorithms. This would reduce the need for custom implementations, which could introduce errors. Additionally, tooling should be available to support formal verification and testing of programs written in the language.

A language with these features would be well-suited for being written by a language model and verified by humans and formal verification systems. However, achieving a completely provable and error-free language is still an open challenge in the field of programming languages and formal methods.

Similar languages today

Then, I wanted to know what languages today are close to this ideal:

Me: Which existing language is closest to this?

GPT4: There isn't a single programming language that perfectly fits the description of an error-free, provable language, as different languages have various strengths and weaknesses. However, there are a few languages that come close in terms of their focus on safety, formal verification, and simplicity. Some of the most notable ones are:

1. Coq: Coq is a formal proof management system that provides a functional programming language called Gallina, which is used to express mathematical assertions, mechanically check proofs, and extract executable code. Coq is used in various projects that require strong guarantees of correctness, such as the CompCert C compiler and the development of formally verified cryptographic algorithms.

2. Agda: Agda is a dependently typed functional programming language that is also a proof assistant. It allows users to express and prove properties of their programs using dependent types. This helps to catch many errors at compile-time and provides a high level of assurance in the correctness of the code. Agda is often used for research in type theory, programming languages, and formal methods.

3. Idris: Idris is another dependently typed functional programming language that is similar to Agda but with a stronger focus on practical programming. Its dependent types allow for the expression of rich specifications that can be verified at compile-time, leading to safer and more robust code. While Idris is not as widely used as Coq or Agda, it provides an interesting blend of practicality and formal verification.

4. Ada/SPARK: Ada is a statically typed, high-level programming language designed for safety-critical systems. Its subset, SPARK, is specifically designed for formal verification and has been used in the development of safety-critical systems, such as aerospace and defense applications. SPARK provides support for contracts (preconditions, postconditions, and invariants) and allows for formal verification using proof assistants and automated theorem provers.

While these languages come close to the ideal of an error-free, provable language, they still require a significant amount of human effort and expertise to write and verify correct programs. Additionally, each language has its own trade-offs in terms of expressiveness, ease of use, and performance.

Designing a new language

Finally, I asked GPT4 to design a language that meets those requirements and give me some examples:

Me: Take a subset or intersection or extension of these languages so it meets the criteria, or is closer to the criteria than these languages, and make up a new simpler language from this. Give me a few examples written in this new language

GPT4: Let's create a new, simpler language called "VeriLang" that combines some of the best features of Coq, Agda, Idris, and SPARK. VeriLang will have the following characteristics:

1. Strong, dependent typing

2. Functional programming

3. Built-in support for contracts and specifications

4. Limited side effects and immutability

5. Simple syntax and constructs

Here are a few example programs in VeriLang:

Example 1: Factorial function with a contract

-- The factorial function takes a non-negative integer and returns its factorial.
factorial : (n : Nat) -> Nat
{ Pre: n >= 0, Post: result >= 1 }
factorial 0 = 1
factorial n = n * factorial (n - 1)

Example 2: Safe list indexing with dependent types

-- A list with a length encoded in its type.
data Vect : (len : Nat) -> Type where
  Nil  : Vect 0
  Cons : (head : a) -> (tail : Vect len) -> Vect (len + 1)

-- Safe list indexing function.
index : {a : Type} -> (n : Nat) -> (xs : Vect len a) -> {len : Nat} -> Maybe a
{ Pre: n >= 0, Post: (result == Just x) <-> (n < len) }
index _ Nil _ = Nothing
index 0 (Cons x _) _ = Just x
index n (Cons _ xs) len = index (n - 1) xs (len - 1)

Example 3: Verifying a sorting algorithm (simplified)

-- A simple insertion sort function.
insertionSort : {a : Type} -> (xs : List a) -> List a
{ Pre: True, Post: isSorted result }
insertionSort [] = []
insertionSort (x:xs) = insert x (insertionSort xs)

-- Insert an element in a sorted list.
insert : {a : Type} -> (x : a) -> (xs : List a) -> List a
{ Pre: isSorted xs, Post: isSorted result }
insert x [] = [x]
insert x (y:ys) | x <= y    = x : y : ys
                | otherwise = y : insert x ys

-- Check if a list is sorted.
isSorted : {a : Type} -> (xs : List a) -> Bool
isSorted [] = True
isSorted [x] = True
isSorted (x:y:xs) = x <= y && isSorted (y:xs)

These examples demonstrate how VeriLang could combine dependent types, functional programming, contracts, and simple syntax to create a language suitable for formal verification. However, designing a complete language and verifying its correctness would require substantial research and development.

Are you ready?

If we assume that language models will write most of the software in five years, and we assume that humans will have a role verifying the correctness of this software, GPT4 can tell us what this language is likely to look like. From where I'm standing, it turns out it looks a lot like Haskell! So maybe this is another reason for you to learn Haskell if you haven't already.