DIKU Bits: Proof-Carrying Code
Andrzej Filinski, associate professor in the Programming Languages and Theory of Computing section at DIKU.
How can we be sure that a program we want to run is correct, or – less ambitiously – at least free of malware or exploitable security holes? Especially if that program is written in an unsafe, low-level language (like C), or is already compiled to machine code? Maybe we could require the entity who produced the program to rigorously prove to us (or to our trusted electronic assistant) that their code is actually safe? This once-utopian idea is now becoming feasible, thanks to recent and ongoing advances in machine-verifiable proof technology.
Zooming in on Andrzej Filinski
Which courses do you teach? (BSc and MSc)
"Implementation of Programming Languages" on the BSc programme, and "Advanced Programming" and "Semantics and Types" on the MSc programme.
Which technology/research/projects/startup are you excited to see the evolution of?
Formal methods for software development and certification, once employed only for the most safety-critical applications (e.g., avionics) are slowly migrating into the mainstream. Part of the reason is that the raw computational power for machine-assisted reasoning about our code is finally starting to catch up with our ability to write it in the first place. I expect that, over the next decade or two, these developments will profoundly influence the way we write and deploy software systems.
What is your favorite sketch from the DIKUrevy?
That would have to be "Se 'mantikken og dø" (2018, I think). It's good to see our students recognizing that sloppy arguments are at the root of all evil.