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.
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:
Kleene algebra. This is an interpreted formal language theory together with a prescript on how to understand expressions as computer programs.
Algorithmic logic (often referred to as dynamic logic). This is a program notation embedded in a modal logic/ Strictly speaking it is a logic but the expressive power comes from the program notation.
The program algebra PGA.
The theory of program schemes (which has several variations).
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 programming is an industry of formidable size. Computer programs are present in most equipment and computer programs are vital for the operational security and safety for all major systems world wide.
Many processes and procedures find their expression in computer programs. However necessary specifications and requirements at higher abstraction levels may be in many cases the programs themselves contain the description of their intended functionality. There is no objection against the use of programs as means to convey information if the program notations used support that perspective.
Computer programs nowadays live much longer than the computers for which they have been originally desiged. This is very remarkable. It is often simpler for an organization to replace all of its hardware than all of its software.
Since its inception the architecture of computing devices has been remarkably stable. So it seems that the basic primitives (instructions) of programming are known and that not much can be gained from an investigation of those. However, this may well change due to the need to produce highly parallel chips. With the steady increase of processing speed coming to an end only increased concurrency can be exploited in order to obtain higher performance. This phenomenon will lead to a renewed interest in all basic aspects of computer programs and their automatic execution.
Computer programs are so basic for all technology that they deserve foundational investigation from a perspective of pure science. Again the situation is comparable with logic: each specific logic may be dealt with within the subject that makes most use of it, but the totality of logics constitutes an independent subject. Similarly a particular progic may be developed form pragmatic purposes within some branch of computer science. But in spite of that progic in general is an independent topic.
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.
Here are some issues that might be considered as belonging to philosophical progic:
In what sense are computer viruses programs?
Which awareness of progic is needed (if any) if someone is supposed to make safe use of a computer.
Where is the line that separates the programs and specifications that merit (or require) formal verification from those that merit mere testing. And where is the line that separates the progics based on formal testing from progics based on a much more liberal form of field testing? What is the role (if any) of verification by means of hand made proofs (comparable to the majority of contemporary mathematical proofs).
How is it possible that vast numbers of people can be useful programmers while using program notations for which they have no valid semantic theory at hand.
Can computer progic be purely finitistic in the sense that exclusively finite state systems are considered. If not: what makes inifnite state spaces so useful, if so why is it not done that way in practice?
How should one adapt one's programming style to make use of the fact that an execution architecture offers automatic garbage collection? (This feature is advocated as crucial by program notation designers, but books never tell how to make use of the fact!)
What is thashing? Garbage collection takes care of removing objects which have become inaccessible by any conceivable program. Let us define thrashing as the removal of objects which will not be used by a specific program that is being executed. Thrashing is relative to a specific running program. It is obvious that trashing makes little sence if one deals with an unbounded object pool. So suppose that a maximum of K objects can be created, then thrashing may evacuate space that can be used for the creation of new objects. The queston is now: can one make sense of the concept of thash at an informal level? (It should be noticed that a naive approach immediately leads to a paradox. An object may never be used in some computation, but after removing the object more space may be available with the effect that a computation can be extended so far that the thrashed object is made use of once more. Merely declaring all objects that will not be made use of in a computation from some state onwards as thash is not going to work.)
Here is a much more specific question: what is an array? Let it be granted that this question belongs to computer science. Its classification within computer progic is justified by the observation that the term array is dominantly used to explain or identify program notation features. The simplest view of an array is that it is a table indexed by natural numbers (or rather a finite range of those). But in fact it is also understood that 'access is quick'. If the range is a subrange of the collection of integers of some machine (which always turns out to be finite) then it is reasonable to expect constant time access to all array elements. So the intuition of an array is seemingly linked with its indices being chosen as values in some (subrange of a) predefined finite set. That finally clarifies why there is a problem: what remains of the definition of an array if the limitation of index values to a predifined finite set is dropped: are we left with the mere definition of a table (that is the functionality of the array) or is there an algorithmic part of the definition that guarantees fast access?
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).