Practical Theory of Computation on Structures

There are hardly two fields in Computer Science that are further apart than Software Engineering and Theoretical Computer Science. The lack of theoretical foundations in the field of Software Engineering has a counterpart, as the theoretical foundations have not caught up with the development of practical software systems. This raises the question how a theory of computation should look like that modernises the classical theory and at the same time is suitable for practical systems development. This article is dedicated to a sketch of a theory of computation centred around the notion of algorithmic systems. I will argue that behavioural theories are key to the understanding, i.e. we require language-independent axiomatic definitions of classes of algorithmic systems that are accompanied by abstract machine models provably capturing the class under consideration. The machine models give further rise to tailored logics through which properties of systems in the considered class can be formalised and verified, and to fine-tuned classifications on the grounds of complexity restrictions. All extensions are conservative in the sense that the classical theory of computation is preserved, universal in the sense that all practical developments are captured uniformly, and practical in the sense that languages associated with the abstract machine models can be used for rigorous high-level systems design and development, and the logics can be exploited for rigorous verification of desirable properties of systems.