The speaker believed mathematicians who had experimented with Isabelle and other systems were similarly concluding that their desired mathematics required a highly expressive framework.

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