Part of Marianne’s flash of inspiration came from a talk she’d seen about translating programs to a form Z3, a popular SMT solver, can run as proofs. Full of enthusiasm she invites the software engineer who gave that talk, Tikhon Jelvis, to elaborate on the similarities between SMT and code normally generated by the compiler.