Johannes Hostert

Hello there :O

I’m Johannes, a PhD student at ETH Zurich since October 2023. If you ask ETH, they will tell you that I’m a Doctoral Student (ETH), but that’s the same difference. 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 verification, especially using separation logic, as well as type theory in general. Most of my research currently uses Rust in one way or another, but I’m not solely focused on it. That being said, I love how Rust is setting new standards, by showing that one can write fast and efficient programs without compromising on safety. With my research, I hope to make Rust even faster, while also allowing users to establish yet stronger guarantees about their Rust program.

Together with Neven, Ralf, and Derek, I am currently working on Tree Borrows, a new aliasing model for Rust. The goal is permitting the Rust compiler to heavily optimize Rust programs, without imposing too severe restrictions on pointer-manipulating code. I am also thinking about 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 Coq.

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