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 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 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.

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 ❄️