I've been struggling with the notion of theories and provers in the context of computer programming for a long time now. I was reading Peter Naur's general concept of Programming As Theory Building and I don't see how it connects to Type Systems at all.

In Naur's thesis, there are three kinds of objects: (1) The world of physical things and events, (2) the world of mental objects and events (qualia?), and (3) the actual products of thought such as theories, stories, myths, tools, and social institutions. Programming, Naur says, is about the creation of objects of the third kind: the reification of thought products into processes. It isn't enough to be intelligent; one can intelligently and skillfully perform all sorts of actions such as driving, typing, dancing and so forth; one must also have a theory, a context backing your actions such that you can meaningfully and coherently explain your theory, answer questions about it, argue on behalf of it.

In Naur's Theory Building View of Programming (1985), the act of programming is the construction of a theory about how human processes can best be supported by one or more computer programs. This sorta coincides with Yourdon's premise (1989) that one can't begin to cybernize (Yourdon's word) a process until one clearly understands the process he is seeking to enhance or replace. Prior to the Age of the Internet, Systems Analysis and Design was a serious discipline (I'm a Trained Cyberneticist™, kids, don't try this without professional help!) in which the first step was to completely document the end-to-end product of some paper-pushing organization, and then try to figure out how to best enhance or replace that organization's paper-pushing with a more efficient computerized version. It wasn't enough to replace notebooks and carbons with keyboards and screens; sometimes, you had to replace whole systems with streamlined or adapted versions. We were taught that Analysis and Design was a holistic discipline, not just a programmatic one.

One place where I think Naur breaks down, and this may be due to the tools and processes available to him at the time, is where he says that he believes it is impossible to embed enough of the Theory (the outcome of the original team's analysis and design) in any given program for it to be clear to other programmers without further input from the original team. The Theory is clear only in the team's collective intelligence as they develop the program, and the program only articulates some mechanistic processes that support the theory.

I also believe that Naur falls down in the face of modern development because the disciplines of programming simply weren't all that great in the 80s. Too much of it was dedicated to trickery to get more performance out of the system; the Theory embodied not just what the program had to do, but specialized assumptions about the hardware that would support it. Finally, programs today are built from tens, perhaps dozens, or even hundreds of libraries; I don't believe we actually need a Theory for each library to competently use them in our productions.

I do believe we need a Theory for our own production, to explain why we need so goddamned many libraries, however.

Naur claims that few software development houses work according to a Theory. He may be right. There are tens of thousands of "IT shops" in this country, and most of them don't really care. They just want to develop Yet Another App, their knowledge of the underlying technologies, be they HTTP, SSL, virtual machines, containerization services, and databases, is so tenuous as to amount to empirical daemonology: poke it and see if it pokes back. But that doesn't matter, as CPU power is cheap and there's enough scaffolding holding the whole leaking, clanking, steaming, whistling contraption to lurch forward like Howl's Moving Castle, such that they don't have to care. There are days when I feel like I'm working with a theory that is, at best, vague and hard to define.

As near as I can tell, the terminology of "theory" in Type Systems has some overlap to Naur's: The programmer uses Types to constrain what the program does to fit within the Theory in the programmer's head, and uses the Type Checker to assert that the Theory is complete and comprehensive, but I don't think that the notion of "provers" in Type Systems has anything to do with Naur's thesis.

Naur's Programming as Theory Building is still relevant 30 years after its publication (and the year I started my CS degree program), but it describes challenges most of us no longer face, and was written at a time when the cognitive support tools were a desert wasteland compared to what we have now. It's worth reading, and it's worth supporting, because if you write software and you don't have a clear theory about what the program will be and what it will do, you can't write a good program.