PROGIC is a phrase that I propose to use in a way similar to logic. Whereas logic is about the expression of properties progic is about the expression of programs. A progic is a metatheory about programs that brings with it an informal notation, an intended meaning for that notation, examples of its use and preferably some useful metatheory. Different programming styles lead to subcategories of progic: imperative progic, functional progic, logical progic. The default meaning of progic is 'imperative progic' very much like a default meaning for logic might be 'classical logic'.

Progic stands to programming as logic to reasoning. Programming is 'progical' if it follows some precise theory of programs, i.e. some well-worked out progic. Reasoning is logical if it conforms some well-understood logic. In practice programming is often not progical an reasoning is (often) not logical. Progical programming is an ideal which is very hard to achieve. But is seems to be a defendable position that only progical programming can produce programs which can be proven correct.

Computer progic is a part of progic. Its characteristic aspect lies in the permanent awareness that pgrograms are meant to be executed by a computer. In practice that means that computer progic has a focus on lower level features than progic at large.

Some examples of progics

Progic can be performed in a mathematical form (mathematical progic), or in a philosophical form (philosophical progic) or in a engineering form (engineering progic or software engineering). In each of these cases a theoretical and an experimental form of the topic may be distinguished. Typical examples of (mathematical) progics are:

Why progic

PROGIC is not a new term, it has been used for "probabilistic logic", but the use seems to be a rather pragmatic decision to find a name for a conference without further ambition. The motivation for coining a new term to denote an entire field stems from the observation that computer programming is notoriously hidden as a supporting theme or topic in computer science, which itself is becoming a less and less visible part of informatics at large.

Here are some properties of computer programs which make them a valid and independent subject:

Computer Science = Computer Architecture + Computer Progic

It can be defended that nowadays computer science is a proper part of informatics. Computer science has a focus on the tools (computers) which trancends the focus on their application. One might then contemplate the following identity:

'Computer science = Computer architecture + Computer programming'

But there is an unfortunate mismatch between architecture and programming. The term programming suggests an active and application oriented attitude which is in no way implied by its counterpart (in the equation) architecture. In progic the programs themselves are of equal or higher importance than the human activity that leads to their coming about. Progic can be defined in its role in this equation for computer science:

'Computer progic = Computer programs + Computer programming = Computer software science'

In this jargon computer engineering is not a part of computer science, the science is about the engineering at best. Conversely computer science might be considered a part of computer engineering perhaps, in which case one arrives at the equation 'computer science = theoretical computer engineering'. Similarly software engineering need not be considered a part of computer science. Indeed more often than not software engineering involves so much domain specific knowledge that its, strict inclusion in computer science cannot be maintained.

Questions in philosophical progic

Here are some issues that might be considered as belonging to philosophical progic:

Questions in mathematical progic

Open issues in mathematical progic abound. I will formulate only one on this page. Suppose a program notation is required to view programs as finite or infinite but cyclic sequences of instructions. And suppose that the meaning of a program is a thread in the sense of thread algebra. Further assume that there is only a finite set of instructions that may be used and finally suppose that each finite state thread can be denoted by one or more of these programs (instruction sequences). It is known that no finite state execution mechanism can process all of these programs. We conjecture that an execution architecture which can process all programs (in the given notation) and thereby generate all finite state threads cannot be designed if it can only use a stack as an auxiliary service. A 'stronger' service is needed but that stronger service need not be as strong as two stacks (that is it need not be Turing complete).