As it happens, I would like to rehearse a talk I am giving at CS on Thursday.
It is difficult (some would say impossible) to demonstrate that we have designed software reliably unless we use a formal description language. For many years such languages were only applied at levels of software lifecycles which are close to the code itself (most notably in verifying properties of specifications). However, it has been observed that most of the cost of producing software is in earlier stages of requirements analysis and high-level modelling of systems. We are only beginning to understand how formal methods may be applied to these stages. One of the main distinguishing factors of high level design is that problems are loosely constrained and there is much greater need for standard practice in knowledge acquisition and design refinement. This, in turn, shifts the balance of research away from a "pure" study of the semantics of formal languages towards studies of the pragmatics of language application. Fortunately, many notions of pragmatics can be understood in a formal, abstract way which allows us to discuss many of the key notions independently of the domain of application. I shall survey recent Edinburgh work from this point of view; summarise how it has been applied; and suggest areas of further work.