Will Crichton: 'How to Make Mathematicians Into Programmers (And Vice Versa)'

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.

[markdatko]

Extremely interesting video especially in researching my "autobiography" from the
FORTRAN and punch card days in the 1970's to exploration of Haskell and Lean in the 2020's

[dmitriidemenev]

I was both interested in Rust and mathematics but I could not imagine you appearing on Topos Institute channel. It was a pleasant surpise.

[veztron]

Great talk and calls to action. Really nice to see Will's perspective here.

[fbkintanar]

11:07 "the trade-off between memory versus perception" ... :"humans have really bad memories":
Another way to look at things is that humans are really efficient at pruning what they don't find relevant. Forgetting is a major principle of structuring cognition and memory, as much as the countervailing principle of retaining.
We can also look beyond the percept to the external world which gives structure to the percept. We can even consider a theory of extended mind, that incorporates the world into cognitive states. I wouldn't necessarily go that far, but I do think an individual mind instantiates some social type context of shared lexicalized concepts. What structures that schema of lexicalized concepts (or in math, notationalized concepts) is sometimes the objective world, but sometimes also social institutions and culture. This is something that LLM-based AI doesn't have, making its outputs and hallucinations opaque to conceptual inquiry or ethical accountability.

[XYReason]

I liked the televangelist microphone. This guy has some sense about the aesthetics.

[ally_jr]

Great Talk! Will is a great teacher/communicator, and clearly very skilled! I read his paper, "A new era of systems programming with Rust" at least once per month to recenter my thinking. Thank you for this paper Will.

[raticus]

For Will: check out the book "Badass: Making Users Awesome". It's an interesting take on skill acquisition.

[MarkGritter]

I thought the point about new users not knowing how to search matched my experience as a new user of F* and Liquid Haskell very well. There is a lot of things in the standard library, and also some things that are just not there, and it was hard to tell the difference or figure out if I really was looking in the right place. (I think the problem is a bit different in Lean which has a more mature standard library, though.)