Human Judgment as a Specification

Well, taking the example in the article about a formal verification to determine whether a regex is for a collection of phone numbers or countries, and if a country is specified as "America", to formally verify whether that means North America or all Americas including the Caribbean:

A regex which "properly" determines this in a witness/formal verification model is subject to the same sorts of political distinctions and nuances, right down to subjective interpretation of which nation-states are legitimate, etc, that participation in warfare/predation/injustice are.

If the USA says that Cuba is part of the USA, and the rest of the Western Hemisphere says it's not, then the formal verification is necessarily matching the prompt intention to a social and political milieu, which, while subjective, is still cognizable and subject to introspection and, in some cases, a type of consensus.

It seems similarly possible to formally verify that results do or do not meet similar subjective-but-cognizable criteria: does the result trigger engagement of weapons systems? Does it they implicate borders in a way that diminishes the sovereignty of a people? (which, like the regex example, have subjective but cognizable nuances)? Does the result serve to enrich (a perhaps pre-supplied) list of criminals/cartels/contractors/war profiteers? All of these seem like similar problems to the regex example.

I don't disagree with your high-level contention that powerful dual-use technology can always cut through the good and evil in each of us. But I think that's precisely the point of searching for formally-verifiable spec-elucidation. If it were obvious from the outset whether or not a particular word represents the same of a nation-state widely regarded as sovereign, or whether an action was or was not an act of war, then we'd not need AI (let alone formal verification of a prompt-result match) in the first place.

That's a really great reframing: "predictability"

...I think we've been exponential (or s-curve) w.r.t. repeatable predictability that _smaller_ prompts are yielding. eg: `regform.php: register( first, last, address, email )` would have had a 30% "one-shot" outcome 1-2 years ago, but closer to 90% "one-shot" outcome this year.

Smaller prompts == wider outcomes... potentially wider (larger?) prompts == smaller outcomes?

As we're "committing" code (blacksmith-type), presumably it's b/c we've reached a plateau of "probably works right" and includes some level of testability and fitness-for-purpose, ie: we've rolled the dice enough times and are committing the current "yahtzee" board to the repo.

16 years ago I've been advocating effectively that "acceptance tests are more valuable than the code under test" (b/c given sufficient acceptance tests, it's "trivial" to reproduce the code correctly... but given the code and no tests it's at least an order of magnitude harder to prove correctness)

http://www.robertames.com/blog.cgi/entries/to-upgrade-or-not...

It's again the dual hourglass shape of consensus between creation and acceptance, and LLM's (when used well) are helping to compress the two sides together around an "exact" agreeable crystallization.

"I want you to calculate pi" (wide hourglass) ...etc... [(precise code/assembly) (precise validation)] ...etc... "pi should start with 3.14", "pirr should equal area", ...etc...

...but throughout time, we as developers have been the human interpreters / vessels via "english-to-buggy-code", and now we have this whole new set of (semi-unpredictable) tools. Think of woodworking (hackers), with hand-tools and eventually moving to power tools w/ jigs. Some things are lost, but others are gained! Maybe we're needing to come up with "jigs" (or "harnesses?" ;-) to strap around our new LLM power-tools?

Closing thought... I've done some sketchup modeling, eg: mocking my kitchen to consider a remodel. "Models must represent to a precision useful for their purpose". Counters, sink, fridge... cool! But then, should I include the toe-kick cutout, or cabinets == flat boxes? Should I include the counter overhang? What about representing the cabinet doors? Should I include the cabinet knobs? Should I actually measure the true openings down to the 16th inch? Validate that they're 90deg rather than 88deg square? On the counter overhang, should I include the rounding? What if it was routed, is the shape of the overhang important?

Basically, reality has infinite detail and our "captured models" of the problem domain are always working at a level of detail that is "fit for purpose". Design a nuclear power plant? LLM == "probably not". Design a local CD ripper GUI for yourself? "the level of detail and correctness is probably fit for purpose"