How to Make Mathematicians Into Programmers and Vice Versa

Explore a thought-provoking colloquium talk that delves into the challenges and opportunities of bridging the gap between mathematicians and programmers through formalized mathematics (FM) tools. Learn about the growing capabilities of proof assistants and model checkers in addressing real-world mathematical and software development problems. Discover how psychological research methods and cognitive theories can be applied to understand and improve the user experience of FM tools. Examine the importance of developing effective educational curricula and tooling for both mathematicians and programmers, with a focus on systematic investigation through lab studies, IDE telemetry, and cognitive frameworks such as working memory and mental models. Gain insights into how these approaches can lead to more informed predictions about the effectiveness of curricula, tooling, and language design in the field of formalized mathematics.