HN Theater @HNTheaterMonth

This video was recorded at Code Mesh LDN 18 http://bit.ly/2P7SPII

Get involved in Code Sync's next conference http://bit.ly/2Mcm4aS

---

HOLISTIC SPECIFICATIONS FOR ROBUST CODE
by Sophia Drossopoulou

THIS TALK IN THREE WORDS:
Robust
Specify
Information hiding

TALK LEVEL: Beginner

ABSTRACT
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.

This is joint work with James Noble (VUW), Mark Miller (Agoric), and Toby Murray (Univ. Melbourne)

Read the full abstract: http://codesync.global/speaker/sophia-drossopoulou/

---

THE SPEAKER - 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.

More on Sophia Drossopoulou: http://codesync.global/speaker/sophia-drossopoulou/

---

CODE SYNC & CODE MESH LDN 18
Code Mesh LDN is powered by Code Sync. Code Mesh LDN 18 was sponsored by WhatsApp, Toyota Connected, Erlang Solutions, TEAMango, and aeternity.

CODE SYNC
Website: www.codesync.global
Twitter: www.twitter.com/CodeMeshIO
Facebook: https://www.facebook.com/CodeSyncGlobal
LinkedIn: https://www.linkedin.com/company/code-sync/
Mail: info at codesync.global

#CodeMesh #Robust #Specify #InformationHiding #SophiaDrossopoulou