The Intent Envelope: Proofs for Completeness, Not Just Soundness
5 points by heyyfernanda
5 points by heyyfernanda
Would be awesome if the author showed an example of a proof (in code). The article seemed to end a bit too early...
EDIT: or was the four lines in the "Writing Proofs" section it? No Lean-like telling it why it is true, just stating what you want to be true?
Thanks for the feedback. I was trying to lean more conceptual than technical in this post, but point taken that some code would be useful.
Here’s an example of code from our multi-collaboration kanban project:
I am quite surprised to see no mention of postconditions, which are what we normally call these "intent envelopes". It might be helpful to think of your "envelope" as a set whose elements are each acceptable states.
Previously, on Lobsters, I showed by example how important it is to write with precision and clarity when writing prompts. Today, I want to explain how to use the em-dash in order to emphasize that conventions and grammar also matter. First, in this sentence:
We’ve been building toward correct-by-construction systems — using Dafny to formally verify that implementation code matches spec before it even compiles.
The em-dash can be replaced with a preposition like "by" which subordinates the second clause. The preposition can be ambiguous about whether it binds the verb "building" or the noun "systems".
We’ve been building toward correct-by-construction systems by using Dafny to formally verify that implementation code matches spec before it even compiles.
Second, in this sentence:
Not just that it won’t accept invalid actions — but that it won’t reject valid ones.
The em-dash can be replaced with a comma because the second clause starts with a logical connector "but", which performs an AND operation. Sometimes the comma can be elided if the first clause is sufficiently simple, but the logical negation "not" at the beginning forces the two clauses to be treated as subordinate to a clause in the previous sentence. Nonetheless:
Not just that it won’t accept invalid actions, but that it won’t reject valid ones.
With the awkwardness clearly exposed, we might rewrite the entire paragraph using a more subjunctive mood. The logical connectors in English must be reconjugated from "not/or" to "neither/nor".
This creates a verification challenge: proving that a system is flexible enough since it ought to neither accept invalid actions nor reject valid ones.
The paragraph still is awkward, but the em-dash is fixed. (Exercise for the reader: can the colon be removed somehow?) Another comma example is from this sentence:
The server can’t always do exactly what was asked — but it can try to preserve the intent.
We can remove the em-dash entirely:
The server can’t always do exactly what was asked but it can try to preserve the intent.
Finally, in this sentence, the em-dash ought to be replaced by a colon because it begins a listing:
Proofs verify the structure directly — no sampling, no enumeration.
The key is noticing that each element of the listing has a common prefix, "no" in this case. The beginning of the listing is always a colon.
Proofs verify the structure directly: no sampling, no enumeration.
When a listing needs to be broken out into a subclause, it can be surrounded by commas. That's one of two ways to fix the following sentence:
The predicate takes two actions — the original request and a candidate alternative — and returns true if the candidate preserves the intent of the original.
By turning it into:
The predicate takes two actions, the original request and a candidate alternative, and returns true if the candidate preserves the intent of the original.
This works because the two elements are joined with a logical connector and don't have their own commas inside. If we were to have more elements then we could nest with a semicolon, taking advantage of the fact that Oxford commas don't cost ink on computer screens, then we might write:
The predicate takes three actions, the original request, a candidate alternative, and a secret third thing; and returns true if the candidate preserves the intent of the original.
At some point, listings ought to be broken out into explicit enumerations. Here, we can compromise by using a full stop to delimit the listing instead of a semicolon, so that the sentence is broken into two pieces and a colon can be used to properly start the listing:
The predicate takes three actions: the original request, a candidate alternative, and a secret third thing. It returns true if the candidate preserves the intent of the original.
I feel like I've missed some context.
I want to explain how to use the em-dash
The following is about how to remove the em-dash in various scenarios. Is this tongue-in-cheek for "we should never use em-dashes"?
I have enjoyed using dashes (em, en or otherwise) for decades. I feel they are particularly useful when writing in a speaking style. Of course we can use various punctuation with precision and clarity, but the link is to a blog not an academic article (which, to be fair, often lack clarity and frequently precision) so "writing in a speaking style" is par for the course.
Of course there is the whole "LLM is bad" + "LLM uses em-dash" = "writer must be a poser" thing going on right now too - is that the subtext? Otherwise the advice seems solid, with good tips of how to achieve clear and precise writing using the punctuation taught in primary school. Maybe that is itself a shout-out to the Midspiral company which seems to want to combine natural language and formal verification?
(I think my reaction here is because I believe the purpose and intended audience should guide the writing style rather than there being "one true style" for all writing).