<

Sophia Drossopoulou

Professor, Imperial College London

Sophia is Professor of Programming Languages at Imperial College London. She started her career in research in compilers, and in particular parsers and attribute grammars. But then she was drawn into the beautiful world of programming languages, and what can be expressed naturally and succinctly with the right choice of paradigm. Since then, she has been working on type systems, module systems, ownership types, traits, type-state and session types for oo languages, and concurrency. With her students, they were the first to propose gradual typing and type inference for Javascript. She is passionate about getting to the bottom of things, and formulating the most elegant and precise explanation.

Past conferences

Sophia Drossopoulou
Code Mesh LDN 2018
08 Nov 2018
15.35 - 16.20

Towards specifications of robustness -- the things that programs do _not_ do (BEGINNER)

Programs are considered to be robust, if they behave “well” in all possible usage scenarios, whether intended or not. To help develop robust programs several programming language features and programming patterns have been proposed: constants, private members, encapsulation, capabilities, ownership, proxies, membranes etc. All these are powerful mechanisms which support the development of robust code.

However, these mechanisms do not address the question as to what specific guarantees we want the particular robust code to make. How do we express, eg, that a DOM-tree protected by a wrapper will not be modified beyond the part allowed by the wrapper, or that money will not disappear from a multiowner-account unless one of the account holders withdrew their money? Traditional program specifications, based on pre- and post- conditions do not address robustness either.

In this talk we will claim that robustness is about guaranteeing that certain thing will not happen – as opposed to functional specifications which are about what will happen. We will introduce "holistic specifications", an extension of traditional program specifications that support the expression of robustness properties through a logic with spatial and temporal features. We will show how holistic specifications can be used to specify robustness concerns in a number of popular program patterns from object-capabilities and smart contracts: the membrane, Mint-and-Purse, DOM-wrappers, the DAO, and ERC-20. We will show how to reason about the preservation of non-trivial properties concerning our data when it comes into contact with unknown, or adversarial code.

OBJECTIVES

To discuss what _is_ robustness, and how to specify robustness aspects of programs.