Reasoning between Programming Languages and Architectures

The amazing complexity of today's programming calls for a newengineering approach to build robust systems. Recent progress informal methods and mechanised proof assistants have made it possibleto apply mathematically rigorous methods to the specification, testingand verification of ambitious projects. Nevertheless, despite someremarkable successes, working with full-scale, realistic, systeminterfaces is still in its infancy and novel tools and reasoningtechniques are needed to support a major change in the engineeringpractice. In this spirit, each chapter of this mémoire d'habilitation proposes asolution to a problem arising from programming experience:Chapter 1 points out how shared memory is a subtle model ofcomputation, and shows how to rigorously build sound abstractions ofthe relaxed memory exhibited by mainstream programming languages andarchitectures;Chapter 2 illustrates how hard concurrency problems, as huntingconcurrency compiler bugs, can be made tractable via semantictechniques that enable thread-wise reasoning;Chapter 3 discusses the difficulties of formalising languagedefinitions, introduces the Ott tool for the working semanticist andreports on five years of user feedback;Chapter 4 explores the design space to integrate typed and untypedcode in scripting languages and presents a sweet spot whereprogrammers benefit from the best of the two worlds.Each chapter ends with some open research directions that, in myopinion, constitute necessary and significant steps towards makingmodern systems easier to program, analyse and test