An obvious response to these observations is to broaden the net of application of FMs. This is exactly what Exotic-FM is striving to do. An advantage of specification and verification in a non system development setting is that the problem of mapping to implementations often does not arise. This is because such application areas typically use formal methods solely for modelling and analysis, without the intention of generating an implementation in the computer science sense. Abstraction can be important in these exotic application areas since programmed interpretations are often too prescriptive and only a loose description of the system under investigation is possible.
Formalization brings the possibility to verify the resulting description.
Many different forms of verification are possible - reasoning about the description using theorem proving technology, model checking to automatically determine if a particular property holds or even doing performance analysis to determine the varying behaviour of the system. All such techniques have potential relevance for exotic application areas. To indicate the spectrum of possible exotic applications, I list some possible topics. These have arisen out of a quick brainstorm between myself and Tommaso Bolognesi and are either topics where we know some formal methods work has been done or where we have some intuition that the area could be amenable to formal interpretation. A major element of this is formally interpreting cognitive architectures and it has some history.