Formal methods in HCI are important for providing applicable theory with the overall aim of improving interactive systems, especially safety critical systems. But formal methods are notoriously difficult, and there are severe limits on the complexity of interactive system specifications that can be explicitly handled.
This paper shows that computer algebra systems, which automate doing mathematics, can make substantial contributions to the work of doing formal HCI, whether for research or development. Formal interaction specifications can be generated, and theorems explored, and all this can be done automatically directly from full, runnable implementations. Conventional iterative design may modify these implementations, and it is then trivial to automatically re-run the formal analyses, which can be re-generated automatically from the modified programs.
Get Mathematica or a reader from Wolfram.