HCI Seminar - Shriram Krishnamurthi - The Human Factors of Formal Methods

Speaker
Host
Abstract:
"Formal methods" include specification, programming, and more: from logics to express desired program behavior to algorithms to check correctness. Lean is a formal method, SMT is a formal method, LTL is a formal method, Rust's type system is a formal method. As formal methods improve in expressiveness and power, they create new opportunities for non-expert adoption. In principle, formal tools are now powerful enough to enable developers to scalably validate realistic systems artifacts without extensive formal training. However, realizing this potential for adoption requires attention to not only the technical but also the human side—which has received extraordinarily little attention from formal-methods research. This talk presents some of our efforts to address this paucity. We apply ideas from cognitive science, human-factors research, and education theory to improve the usability of formal methods. Along the way, we find misconceptions suffered by users, how technically appealing designs that experts may value may fail to help, and how our tools may even mislead users.
Bio:
Shriram is the Vice President for Programming Languages at Brown University in Providence, RI, USA. He’s not, really, but that’s what it says on his business card. At heart, he's a person of ill-repute: a Schemer, Racketeer, and Pyreteer. He believes tropical fruit are superior to all other kinds. He is terrified of success, because he may be forced to buy a suit. On a more serious note, he's a professor at Brown who has created several influential systems (such as DrRacket, Margrave, Flapjax, and Lambda-JS) and written multiple widely-used books. He has won SIGPLAN's Robin Milner Young Researcher Award, SIGPLAN's Software Award (jointly), SIGSOFT's Influential Educator Award, SIGPLAN's Distinguished Educator Award (jointly), and other recognitions.
This talk will also be streamed over Zoom: https://mit.zoom.us/j/97298991671.