After working with Roc for a year, the speaker concluded that dependent type theory could support the mathematics he wanted to formalize.

“And so after my year working with Roc, it became clear to me that this was the framework that was capable of, of doing that type of mathematics. Um, and I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions that to do the mathematics that they wanted to do, they needed this very expressive framework.”