This invited talk looks at “how to bring the other 90% into the fold” of formal methods with a focus on education, comfort with formal methods and effectiveness with formal methods. This focus leads to emphasizing model finding such as the Alloy verifier, SAT solvers and SMT solvers over deductive methods.
User experience is briefly discussed – mentioning that model finders are “often integrated into higher-level tools (with their output presented in a domain-specific way)”.
The main focus is on education and especially creating specifications which is based on an analogy to the author’s “How to design programs” book that breaks creating a program into seven steps starting with designing I/O data structures and examples and ending with testing. Each of these steps leads to distinct artifacts. This builds on a lot of cognitive theory from education research and the notion of “concreteness fading” as design goes from concrete examples to more flexible/abstract/generalized code.
In an educational setting, they can lean on the availability of “ground truth”: the instructor already understands the problem and has a solution. This allows any artifacts (e.g., examples) developed during the design process to be automatically checked against the instructors solution and feedback given in the form of new examples for the student to consider. (The author’s have published about this before in the context of program design.)