Topos Institute Colloquium, 22nd of August 2024.
———
Tools for formalized mathematics (FM), such as proof assistants and model checkers, are increasingly capable of handling the real-world problems of both mathematicians and software developers. Yet, these tools are only as effective as the people who use them. The FM community clearly needs to invest in better education and better tooling. But... which curricula are actually effective for learners? What tooling will actually make users more productive? In this talk, I will lay out some preliminary ideas for how to systematically investigate these questions, i.e., develop a science of human factors for FM. My core proposal is to combine experimental psychological methods (e.g., lab studies, IDE telemetry) and cognitive theories (e.g., working memory, mental models) to study how people use FM tools. Then that understanding can be applied to make principled predictions about the efficacy of curricula, tooling, and language design.