System Modeling Challenges

Some of the discussion in the Correct by Construction panel is concerned with designing languages to take verification into account. Do we know which features of current languages really need to be changed because they have severe and avoidable repercussions (which should be apparent from the theory), vs superficial aspects which result in minor engineering complications for verification tools?

Better still, can we fulfil the dream articulated by Hoare (``Varieties of programming language'', unifying theories), Abrial (at the VSTTE meeting) and many others for a long time: rather than a fixed ``language'', a program should be specified and implemented using a selection of notations suited to the particular system. Theory should account for reasoning principles associated with these notations and in particular guide the design of sound tools, no more complex than necessary for the particular selection of notations.

Here the relevant theory is not just semantics for programs / designs / requirements models but also logic, e.g., for sound scripting of integrated proof techniques using decision procedures etc.

Reynolds' Idealized Algol is a good example of combining two sorts of notations in a way that retains many properties for reasoning etc. Boerger's incremental developments of Java/C# similarly builds relatively orthogonal layers. How close are these examples to Abrial's engineering considerations; is smaller granularity of language features needed? what about "features" in the sense of restricted forms of constructs, e.g. linear or affine lambda terms, threads with bounded or disjoint heap.

The decomposition and modularization techniques needed here have to support the analysis of run-time features; logical structure alone is insufficient to guide the separation of different concerns engineering needs force us to make explicit. Good theoretical concepts for decomposition and modularization that take behavioral aspects into account are still a challenge.