Abstract

The prevalence of sophisticated (and unsophisticated) cyber-attacks presents a significant threat to modern society. Part of the problem manifests itself in the software underlying the internet, and the myriad of devices on the so-called “Internet of Things”. Whilst useful advances in software development have been made over the last decade or more, it is perhaps surprising that the underlying programming languages have not changed significantly. For example, Java is more than twenty years old and, in that time, has undergone only cosmetic improvements. The question is: what should a programming language of the future look like? I hope to give a glimpse of one possible future.

In this talk, I’ll employ live coding to demonstrate a new language that represents a step-change improvement over the status quo. This is the Whiley programming language and its accompanying “verifying compiler”. The language is focused on ensuring programs meet their specifications. Programming in Whiley feels surprisingly natural and the benefits from including specifications are immediately apparent. The language has been used for the last three years to teach a large undergraduate class about program specification, and we have benefited considerably from this experience.

Bio:

David (@whileydave) graduated with a PhD from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David’s PhD thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC . His interests are in programming languages, compilers and static analysis.

Since 2009, he has been developing the Whiley Programming Language (whiley.org) which is designed specifically to simplify program verification. David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPG As; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.