Johannes Hostert

Hello there :O

I’m Johannes, a PhD student at ETH Zurich since October 2023. My advisor is Ralf Jung, and I’m part of our PLF lab. My name is pronounced [joˈhanəs hɔs’tɐt].

My research interests are program semantics and program verification, especially using separation logic. I also like dependent type theory. Most of my research currently uses Rust in one way or another. I love working on Rust,mostly because of its community which sets and meets high standards of performance and correctness, to which I hope to contribute.

I am currently continuing work on Tree Borrows. Tree Borrows is the formal underpinning for many of the optimizations that make Rust fast, and it is also much more permissive than its predecessor. I am also pondering how existing Rust verification tools can be combined, and made more approachable for people without a PhD in formal verification. Further, I (have students) work on MiniRust, trying to figure out how to give it a formal foundation by translating the definition into a tool like Rocq.

Before I moved to Zurich, I lived in Saarbrücken and did my Bachelor’s and Master’s degrees at Saarland University.

Outside of work, my favourite place in Zurich is the Oberer Letten river bath, which is fun in both summer and winter ❄️