The Brown PLT Blog
Human Judgment as a Specification
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?
Read more…Diagramming Program Values by Spatial Refinement
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:
Read more…LLMs ⭢ Regular Expressions, Responsibly!
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.
Read more…Sharing is Scaring: Why is Cloud File-Sharing Hard?
Here is an actual situation we were asked to help non-technical computer users with:
Read more…Practical Static Analysis for Privacy Bugs
Privacy bugs are deeply problematic for software users (“once it’s out there you can’t take it back”), legally significant (due to laws like the GDPR), and difficult for programmers to find and to keep out. Static program analysis would therefore appear to be very helpful here.
Read more…