Towards strong explainability (debuggability) properties for compiler-generated code

Most code that runs is mediated by compilers -- with their output binaries being the artifacts deployed. These remain a brittle, opaque material: hard to reason about and hard to change (except by re-running 
often-lengthy compilation processes).

This is arguably because the compiler takes at most a best-effort approach to explaining why and how its output models the input source program. We can view compiler-generated /debugging information/ as a kind of operational explanation: the compiler explains its output program state-by-state -- but currently in very patchy ways, often simply incorrectly. (Verified compilation can be seen as taking an 
axiomatic approach, instead of an operational one, to a narrowed version of this problem.)

I'll describe some work that is gradually applying some stronger completeness and correctness properties to debugging information, across a few dimensions: local-variable coverage, call tree recovery, and local-variable "correctness" (f.s.v.o.). Although the most obvious application is to the task and tools of debugging itself, I'll talk briefly about some other applications that this may enable, and why it relates to making software a softer, more malleable material.

bio: Stephen Kell does practical research on programming systems, with the the goal of making computers work for human beings and not vice-versa. His focus is on infrastructure software including operating systems and language runtimes. Some past and present research topics include: realistic formal and metaprogrammable specifications of operating systems' linking, loading and system call interfaces; reflective run-time services in Unix-like processes; using the latter to provide new kinds of dynamic checking in C and other 'unsafe' languages; and making debugging of optimized code more reliable. Currently he has a faculty position at King's College London.