The Brown PLT Blog
The rise of GenAI in programming clearly requires an accompanying rise in formal methods, to confirm that AI systems running wild are producing the solutions we actually want. That in turn requires that we specify what we want. This specification is necessarily mathematical, to take advantage of the formal methods tools. But most programmers know far less about formal specification than they do about programming. What can they do? Compilers can vectorize loops you never wrote. IDEs can finish functions before you do. Agents can refactor your codebase from a sentence. And yet, when you want to inspect the value your program just produced, you still use the REPL as if nothing has changed in fifty years: type an expression, get text back, squint. Here is Python showing you a binary decision diagram: This tool is part of a much broader effort to help us use GenAI responsibly. Please see our newer post with details about the broader context. Here is an actual situation we were asked to help