#53 - RustBelt, Iris, and the Art of Writing - Derek Dreyer

Описание: Derek Dreyer is a professor at the Max Planck Institute, in 2024 he was awarded the ACM Fellowship, in 2017 he got the ACM Sigplan Robin Milner Young Researcher Award. And has participated or lead greatly influential work, such as the RustBelt Project and Iris.

In this episode Derek shares his experience going to Grad School at CMU, how even a great research as himself has fallen pray to the impostor syndrome and how to cope with it. Throughout the conversation he makes beautiful parallels between music and academic papers, and how the work of a researcher is similar to that of an artist an many aspects. He also gives us a few tips about how to become a better academic writer. And of course, we also talked about Rust and the history about formally verifying its type system.

Don't forget to check our [merch store!](store.typetheoryforall.com)

Links
[Derek's Website](https://people.mpi-sws.org/~dreyer/)
[POPL '25 PLMW Talk - How to Write Papers so that People Can Read Them](   • [PLMW @ POPL25] How to Write Papers So Peo...  )


00:00 Episode intro & Derek’s accolades
03:29 Interview begins: meeting Derek Dreyer
04:32 Impostor syndrome & coping in grad school
04:59 Choosing PL & CMU: finding a path
05:08 Early life & school acceleration (Great Neck, NY)
33:05 From niche to impact: why ML modules are hard
34:59 Recursive modules & type theory deep-dive
38:37 How to pick problems & stay inspired
50:13 Max Planck Institute: research model & freedom
1:08:13 Separation logic to Iris: a modern foundation
1:48:02 Rust Belt: verifying Rust’s type safety
2:08:41 Collaborating on OxCaml (modal types in OCaml)
2:14:46 On Rust’s place in the ecosystem (safety vs. ergonomics)
2:17:50 Career advice: feedback, networking & initiative
2:19:24 Closing reflections & thanks
2:21:19 Outro: Discord, store & sponsor appeal