Stanford Seminar - The Human Factors of Formal Methods

()

Formal Methods

SAT solvers can be used to solve technical problems by converting them into SAT questions.
Model-theoretic tools can generate instances that satisfy a given formula, aiding in understanding and articulating system properties.
The output of a SAT solver can expose subtle bugs and help explore pathological instances.
Principled model finding aims to produce instances with richer properties, enabling systematic model exploration.
The speaker's team developed recognized systems like Aluminum and Amalgam for principled model finding.

A study showed that students given a tool with minimal instances struggled, highlighting the need to consider human factors in tool design.
The concept of "intended cognitive impact" emphasizes the importance of visual output design based on perceptual psychology.
Studying models like blob society demonstrates how users inductively derive facts by observing scenarios, applicable to complex systems like security policies.
"Contrasting cases" can improve formal methods tools by using negative examples to help people learn and understand concepts.
The speaker introduces "Forge," a tool that allows users to create domain-specific visualizations to aid in understanding complex concepts.

The Stroop effect illustrates how reaction times are affected by information congruence or incongruence.
The "stoop effect" in visualization occurs when logically related objects are placed far apart, leading to confusion.
Creating visualizations requires respecting spatial, temporal, and other relationships to avoid misleading users.
Domain-specific visual metaphors and epistemically closed input languages can improve visualization usability.

LTL is used in verification, synthesis, and robot planning.
Translating between LTL formulas and English statements accurately is challenging.
A three-year study with 30 active LTL users revealed common misconceptions, including the "exclusive human misconception" related to "x until y" formulas.
Designing logics based on human-centric methodologies and validating usability through empirical studies is crucial.
"Forge" is a tool that helps teach formal methods and includes validated instruments for assessing misconceptions.

Challenges include conveying domain semantics without overwhelming users with unnecessary details.
Enriching semantics with topology or geometry can convey directionality, time position, and spatial projections.
Determining how much semantics to include while maintaining operation validity is complex.
Embedding more domain semantics enables sophisticated contrasting cases and causal models.
Modifying the visualizer's description language to incorporate semantics is necessary.

Formal methods tools should consider the quality of error messages and user feedback.
Designing student-friendly interfaces presents challenges, as exemplified by the speaker's experiences with Dr. Racket.
Tools could potentially educate themselves based on user input, such as administering validated instruments to understand language interpretations.
Tool developers should take more responsibility for improving usability rather than relying solely on user feedback.