Iain Whiteside flirts shamelessy with the practical, but he is never happier than when sketching out a proof on a whiteboard.
Iain thinks that third person is a bit silly for a bio.
When not educating fellow San Franciscans about the merits of the word “faff” or my theory on the division of humankind into four categories, I can be found at NASA Ames Research Center, where I work as a
Rocket Computer Scientist. I work closely with Ewen Denney and Ganesh Pai and, together, we are chipping away at the increasingly important problem of giving a semantics and methodology to assurance cases. I am the lead developer of AdvoCATE, our toolset for developing, maintaining, evaluating, and understanding assurance cases.
My first true love was a lady called Isabelle – unrequited: she treated me very badly, at times – and while I no longer think about her every day, she still holds a special place in my heart.
I wrangled a PhD from the University of Edinburgh back in 2013. My thesis, Refactoring Proof, has the shortest title of my cohort and five Simon and Garfunkel lyrics hidden in it. It defined, and put on a formal footing, refactoring for proof languages in the interactive theorem proving community. With my friend Dominik Dietrich, I made a prototype implementation of a generic refactoring tool based on bidirectional graph transformations, but it has languished. One day I will get back to it.
As a newly minted Doctor, I post-doc’ed with Cliff Jones at Newcastle University on the AI4FM project. Everyone should have Cliff as their boss at some point in their life. Everyone. After another post-doc at Edinburgh University and failing to convince EPSRC that partial functions were important, I dipped my toe in industry.
I have accidentally become an expert in model-driven development, particularly in Eclipse. It has been a very happy accident. The nascent interest, stemming from practical necessity is quickly becoming (and influencing) the central focus of my research.
If one were to invent a common thread in all my work, it is that I am devoted to making the lives of software engineers, proof engineers, safety engineers, and humans easier.
I happen to think that we can teach mathematics a little bit better than we currently do.