Human Judgment as a Specification

blog.brownplt.org · 2,145 words · saved by 3 readers

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? The key problem we’re tackling is: how do we go from the informal (usually prose) to the formal. A natural solution is: use LLMs to translate prose into the formal specifications. On the one hand, this is not absurd: LLMs can do a fairly good job at generating terms in many contemporary formal notations. Here’s Ron Minsky, tongue-in-cheek: I wonder if a more plausible model is, you go to your large language model and say, ‘Please write me a specification for a function that sorts a list.’ And then it, like, spits something out. And then you look at it and thi

Human Judgment as a Specification The Brown PLT Blog RSS CONTACT GROUP PAGE POSTS BY TAG Android April 1 Browsers Crowdsourcing Differential Analysis Diagram Education Flowlog Formal Methods Higher-Order Functions In-Flow Peer Review JavaScript Large Language Models Linear Temporal Logic Misconceptions Permissions Programming Languages Program Planning Privacy Properties Pyret Python Resugaring Rust Scope Software-Defined Networking Spatial Security Semantics Tables Testing Tools Types User Studies Verification Visualization --> PREVIOUS POSTS Human Judgment as a Specification Diagramming Prog

Human Judgment as a Specification

saved by

related reading