The deep link equating math proofs and computer programs

Lacking time to study, is this basically what Phil Wadler has written and talked about, like "Propositions as types"?

To the Mr. Harper's observation we should add that the trinitary theory of computation needs to express itself in reality and it does so thru the quadrant of hardware: transistors, memory, electricity and machine code. Thus three, standing on the four, represents computation in action.

https://softwarefoundations.cis.upenn.edu/ is a great zero-to-hero resource (it's what I used), but to my knowledge it doesn't have an ecosystem review in it. It uses Coq, but the first book has been ported to at least Isabelle, if not others.

I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.

For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.

For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).

For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).

And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).

Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk. However, it does not cover proof assistants.

Alternatively you may enjoy these two. The latter is especially thorough, and begins with classical logic:

* Concrete Semantics (Isabelle): http://concrete-semantics.org

* Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

Types and Programming Languages by Benjamin C. Pierce[0]

[0] https://www.cis.upenn.edu/~bcpierce/tapl/

Since the whole premise here is that formally verifying the properties of programs is equivalent to constructive mathematics, I think you might be asking for too much, modulo your definition of hero.

I'm a fan of formal verification of functional programming. It saddens me to say that, in that line of work, hardly anyone speaks English [0], at least not past the front door. The amount of high-horsery and dog-whistling is enough to wear down any regular folk that walks down the path. Maybe it's the nature of the field itself, that those accomplished folks seem to forget they once walked this earth, up right, on two legs.

[0] read: natural language

There is no such thing as zero to hero for formal methods. It’s a dense and difficult field.

What specific system (programming language) do you recommend to try this?

This is my favorite CS paper of all time. Reason being, it distills multiple different areas of CS down to one idea: state machines. Now I'm frequently able to map a complex idea down to a state machine, which makes all kinds of problems more manageable.

You can also express the "programs as state machines" view in terms of programming language constructs, namely monads (for Time, State and Non-Determinism). If you take a strictly mathematical view of the topic you'll call these 'modalities' or 'modal operators' instead but it's the same deal.

Accessible for who, do you mean? That is in no way 'accessible' without solid exposure to quite a lot of discrete maths (which I have and it's still hard going).

λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ).

Yeah, that's accessible.

Nifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes interesting intuitions, I think. The example derivations with the uncurry example are quite fun to work through. The paragraph about continuations corresponding to double negation is also super neat!

Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.

> I don't get the significance of the Curry-Howard Isomorphism.

* Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust.

Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time.

> What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program?

It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4.

> But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects.

Not every effect is a side-effect. A suitable definition of "side-effect" might be "an effect which is able to punch a hole through whatever type system decided it was valid." If your programming language represents effects as types, then it can reason-about/type-check them just as well as pure functions.

[1] https://www.idris-lang.org/docs/idris2/current/contrib_docs/...

Int -> Boolean is just the type of any arbitrary decidable property on Int's, so it's not very useful on its own. But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. The proof itself need not even be constructive, since the requirement for constructibility was taken care of by providing the code for that function. Constructibility becomes more of a big deal if you want to be able to compose constructive proofs, or write proofs that rely on instances of some other proof as input, since then the strategy of providing some construction as a bare algorithm and separately proving it correct may run into problems.

And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.

I know a Pons Asinorum that kinda was mind-blowing to me. It uses topology connection to define an unexpected function.

"Infinite search in finite time" https://math.andrej.com/2007/09/28/seemingly-impossible-func... https://math.andrej.com/2008/11/21/a-haskell-monad-for-infin...

I don't think you're being an idiot.

There are some connections in mathematics that are quite "magical", where you get something like a correspondence between a family of curved surfaces and a family of integer-valued equations, and it's not at all obvious why that might be until you study it deeply.

And sometimes articles about the Curry-Howard Isomorphism suggest that it's an example of that sort (I think this article does, to some extent).

But (as I understand it), that isn't the case: here we have a simple directly-constructed correspondence. It's valuable, but not the sort of thing that mathematicians think of as a wonderful result.

I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam/ . A lot of logic and theorem proving can be done without ever thinking about CH. In classical logic I think it's not even that convenient anyway, and classical logic is a pragmatic choice.

Hmmm, I can try to address your questions.

1) The trippy one I know of is that the Church encoding of numbers is the induction principle for naturals.

2) Generally the programs that are proofs you would want to be pure, but it wouldn't be strictly necessary. The impurity would have to be handled by the type system though, so explicit effects not side-effects.

Also, note that even though you want the programs-that-are-proofs to be pure, that doesn't mean you can't prove things about programs that are impure - that is, you have a pure-program that has a type, and that type is a proposition about a different impure program.

That is, I can create a pure program that is a proof about my impure program.

EDIT: I think something that is a sticking point for a lot of people is looking for a program that is useful by itself that is also the proof of something useful. This is possible, but a bit rare-er - oftentimes you have useful programs with trivial types, or useful programs-that-are-proofs that you don't actually care to run. These are still super useful though! It is possible to have ones that are both - decidability of things is what comes to mind. You could write a program that determines if two naturals are equal - that's a useful program, albeit one of the simplest - and that program also serves as a proof that two naturals are either equal or not - a kind of particular instantiation of the law of excluded middle. One style of programming with dependent types always returns a proof along with the returned value, which might be kind-of what you're looking for. (Think of a regular expression engine that along with the yes/no does this string match this regular expression, returns a proof that the string does or doesn't match, demonstrating its own correctness)

There are only side effects!

When you compute a pure function, you’re still physically manipulating registers, cache, etc.

You can use the proof-program perspective to formalize reasoning about a program:

- you have some domain model; this expresses the “business logic” of your software

- you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic”

- you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed

Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs.

For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category.

Category theory is the language in which we connect our theory of hardware to our theory of the business domain!

2) Being restricted to pure functions is not actually much of a restriction at all. Any impure input can be trivially replaced with parameterization over values representing that input and any impure output can be trivially replaced by including state updates or the updated state in the return value. Then your entire codebase can be entirely pure and you can let the language runtime or the compiler deal with that pure data at the very top level of the program, performing the IO as needed. This may be slightly more inconvenient than allowing impurity, but not enough that it would be by any means infeasible, and languages like Haskell have facilities which narrow the gap even further, so it's not much of a restriction at all.

Maybe not trippy, but a simple set of examples are existence theorems, i.e. "Given these objects, X exists." An example are fixed point theorems.

Theorem: For any function g from a convex, compact set to itself, there exists a fixed point of g.

program f: g --> x where g is a function from a convex, compact set C to itself, and x satisfies g(x) = x.

If you can write the program and it is correct for all such g, that is a proof that such a g always has a fixed point (in particular, you output one). Note the "type" of g is "function from convex, compact set to itself" and the "type" of x is "fixed point of g".

You won't see many examples of "traditional" languages taking advantage of Curry-Howard. Though you can, e.g. an `Admin` class whose constructor checks that the credentials are for an admin, and functions like `deleteDatabase` which take an `Admin` instance and don't check for admin credentials because they're already "proven".

    loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError>
    deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError>

But 2) is correct: these aren't real proofs, because globals and errors can break Curry-Howard, not to mention unsafe coercions.

    let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) };
    deleteDatabase(evilAdmin, dbConnection, "important_data");

You can't even allow functions which infinitely loop: in theorem-proving languages, every function must be proved terminating. Otherwise you allow:

    anything : a
    anything = recurse 0
        where recurse i = recurse (i + 1)

But in theorem-proving languages, the idea that "this type represents a logical statement, an instance only exists if it's true" is used very often. A classic example is fixed-size vectors

    data Nat where
        0 : Nat
        S : Nat -> Nat  -- n + 1, "S"uccessor

    data Vec (n : Nat) a where
        Nil  : forall a, Vec 0 a
        Cons : forall n a, a -> Vec n a -> Vec (S n) a

You will see declarations like:

    -- Instances of `IsTrue b` only exist if `b = True`
    data IsTrue (b : Boolean) where
        Trivial : IsTrue True

    -- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`)
    data Every (pred : a -> Boolean) (vec: Vec n a) where
        Every_nil : forall pred, Every pred Nil  -- Every item of an empty vector satisfies an arbitrary predicate
        -- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate
        Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs)

    foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil)))
    foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil))

On the other hand, the requirement that all functions must be "logical statements" is essential. Otherwise the programs will crash and the generated proofs will be illogical (and, notice that "crashing program" = "illogical proof"). For example, if one can define the following (impossible to prove) function, one can create programs which crash trying to extract the first element of an empty vector, and proofs which incorrectly assume that all vectors have a first element.

    head : Vec n a -> a
    head Nil = ???
    head (Cons x _) = x

One can define this function though, taking advantage of the fact that there's no such instance `Nil : Vec (S n) a` so only the `Cons` case needs to be matched (which is why this typechecks even though we didn't handle the `Nil` case, while the above example doesn't. Sorry if it's confusing and/or sounds like a cop-out, that's just how it works and real languages accept this kind of pattern matching):

    head : Vec (S n) a -> a
    head (Cons x _) = x
    

And, to answer the second point, theorem-proving languages can represent and prove properties of programs with side-effects and even straight-line programs. The former is commonly done using Monads or Algebraic Effects, and the latter using Hoare Logic or another kind of logic

    data Var a = String

    -- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors
    data IO a where
        Pure      : a -> IO a
        ReadLine  : IO String
        PrintLine : String -> IO ()
        ReadVar   : Var a -> IO (Maybe a)
        WriteVar  : Var a -> Maybe a -> IO a
        (>>=)     : IO a -> (a -> b) -> IO b

    -- "Pure" program which reads first and last name and prints full name.
    -- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values:
    -- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime,
    -- then computes and evaluates `y`
    main : IO ()
    main =
        PrintLine "What is your first name?"  >>= \() ->
        ReadLine                              >>= \firstName ->
        PrintLine "What is your last name?"   >>= \() ->
        ReadLine                              >>= \lastName ->
        Pure (firstName ++ " " ++ lastName)   >>= \fullName ->
        PrintLine ("Hello " ++ fullName ++ "!")

    foo : Var Int
    foo = Var "Foo"

    -- Proving properties of programs is done with Hoare Logic.
    -- This is a lot more complicated and full of boilerplate...
    data Predicate where
        True  : Predicate
        (!==) : forall a, Var a -> a -> Predicate
        (/\)  : Predicate -> Predicate -> Predicate
    data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where
        Obvious  : forall pre stmt, HoareTriple pre stmt True
        Merge    : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2)
        WeakenL  : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        WeakenR  : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1))
    example : HoareTriple
        (foo !== 4 /\ foo !== 5)                                -- Precondition
        (ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1))  -- Statement
        (foo !== 5 /\ foo !== 6)                                -- Postcondition
    example = ...  -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough

> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test.

Did your highschool physics not have this? I always thought it was a universal part of all physics education. Doing things like canceling out units etc. has always been a big part of high school physics, and checking that your final answer has the units it should. (If it didn't, you made a mistake somewhere.)

The idea of building units into Excel is definitely an intriguing one, though. I'm honestly kind of surprised it's the first time I've ever heard it suggested. It does seem like a pretty useful idea.

> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test.

I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).

When I was in high school units were a key part of science education. Is this no longer the case?

Your point about tools that support units is great. Reminds me of https://frinklang.org/

Types and units are very different concepts. In fact it's quite hard to formalize the way units are used in everyday physics.

For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2?

It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way.

Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics.

And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade.

But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.

Most maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problems around velocity, speed, physical quantities etc and you are taught not to mix units, and how units "cancel" etc each other when you deal with exponent laws.

Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education.

I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before.

[1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.

A good way to do this is to replace Geometry class. It is only there because Euclid’s Elements was read by Charlemagne’s kids. Geometry teaches proof, but a very outdated style of proof. It should be replaced with formal proofs, written in Lean or Coq. Since “a proof is a program”, it would also introduce programming into the curriculum.

If I understand what you are asking about correctly, then I do think you are mistaken.

As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.

This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.

Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

Typical proofs don’t cover side channels, just ISA semantics. With the big asterisk that most programs are running on top of an unverified kernel on an unverified machine-level blob on an unverified ISA implemented by an unverified chip, you can absolutely prove the behavior of programs. Lamport has an unusual attitude towards verification and comes towards it from a slightly different angle, and model checking is not a good approach to machine-level proofs.

Note this quote from the article.

"One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox."

This is similar to constraints of making something semi-decidable or recursively enumerable.

Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways.

Some things are easier to find in type theory, other in set theory and for some Turing machines work better.

The Church–Turing thesis isn't provable but is the safe assumption.

IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory.

As an example related to term rewriting which will be important to ML.

https://arxiv.org/abs/2307.14805

I think you misunderstand. On your point about programs not being "provable": it is certainly possible to prove some properties about some programs. It is not necessarily easy, and it very much depends on the program and the property in question, but it is possible.

However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.

What does it mean to say "a program is provable"? You have to prove something about it.

In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.

Most code is so complex that even with the aid of a computer we couldn't run a proof on it if we tried. Most (all!) code also has bugs so if we tried to prove it we would instead prove it doesn't meet requirements. However the theory itself allows that all code could be mathematically proven if you can work around those two issues.

It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.

my first thought was something something dependent types (Idris, Agda), but it also sounds like TS-like structural typing with a Rust-like Result type. proving that every incoming message is either parsed correctly or we return an error seems to be the basic building block. and then every transformation should be other pure functions.

thought I guess you mean something more top-downish? for that there's "program interpretation" ( https://github.com/AdrielC/free-arrow )

and this just looks very interesting https://deepai.org/publication/a-coq-based-synthesis-of-scal...

Ada, not ADA, it's never been an acronym.

And no. Ada is an imperative language with an expressive type system (especially compared to other imperative languages). But it doesn't require things like mathematical correctness/completeness. You may be thinking of SPARK which is a subset of Ada that uses contracts and a prover to prove the contracts hold.

Write the code and proofs in Coq. Coq can output OCaML. I believe OCaML can compile to JavaScript.

That will allow you to verify the pure functions. It will not verify the input/output that will also be necessary.

Depends on the properties you want to verify

Just a head's up, there's an easy way to remember Dijkstra's spelling: D ijk stra. You know, ijk as the common loop indices.

As far as I am aware this doesn’t relate to much work done by Dijkstra. This is really the Type Theoretic computer science program. It starts at Church and progresses through Curry (inspired by Schoenfinkel), then hits the ‘modern’ academic lineage splitting in many directions. On the computer science side in America Constable and his doctoral students (Robert Harper included), Dana Scott, Strachey, Reynolds, the current CMU proof theory/type theory professors, and in Europe you have the French school with Coquand, Huet, etc from INRIA and the English lineage from Milner.

Obviously the above is a very truncated list and misses out on a huge chunk of formative thinkers, and doesn’t get to the cutting edge modern developments. Additionally, I’m leaving out the Math centric developments and people, like Mike Shulman, Dan Licata, etc.

This is all from research way older than Dijkstra.

It does have something to do with his work because his work extended it. But by that metric, it also has something to do with all of computer science, and a lot of mathematics.

Yes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).

I'm not sure. Dijkstra, despite his somewhat incorrect reputation as a curmudgeonly theorist who preferred pencils to computers, had a notable pragmatic streak. And, as a matter of pragmatism, he identified the close relationship between programs and proofs. There are many such examples in his writings, but here are a few[1][2][3][4]. It's particularly interesting to see how his thinking evolves. EWD288 in particular includes what I view as both good advice and a powerful refutation of a fallacy that is stubbornly popular even today:

  Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels.

I have myself applied this in "real" (aka, I got paid for it by a FAANG) programming by proving the correctness of the overall structure of a service (and verifying it with tests) while leaving implementation details for which requirements were nonexistent or unclear unspecified or underspecified. Since I'm neither as creative nor as clever as Dijkstra was I still like to write tests, but I've found that I can do TDD in a way that meshes cleanly with his program and proof construction style. The end result is I have code that I have both proved correct and that has solid test coverage. The tests are particularly useful for collaboration, because it's just not realistic to expect every team member who touches a piece of code to understand and rederive the appropriate parts of said proof. And as an added bonus, it escapes the common complaint for TDD that the tests get in the way of development. They don't when you only test what needs to be proved!

Edit: I find it amusing how much closer Dijkstra's approach is to what might be called "normal" (Algol-ish) programming compared to the Abstract Nonsense[5] favored by the category theorists. I wouldn't call it any less mathematical though. Dijkstra was very much a mathematical formalist as is clear to anyone who has made a study of his work or life.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...

[2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E...

[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

[4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E...

[5] https://en.wikipedia.org/wiki/Abstract_nonsense

Craft similar to painting which AI has overtaken. What we consider programming will go the similar route.