ajaystream

I am going to ignore the form comments -- I guess I am not sure how I feel about being called an LLM (good or bad ?), not sure only time will tell. If LLMs turn out to be the turd of the universe -- bad or maybe good ? -- Emphasis on the '--' for comic interlude

The spec-completeness problem here is the same one that bites distributed systems verification: the proof holds inside an operating envelope (no adversarial inputs, trusted runtime, bounded sizes), and the interesting failures live at the boundary. TLA+ has the same property - you can prove liveness under a fairness assumption the deployment silently violates, and nothing in the proof tells you when reality drifted outside.

What I'd actually want from the tooling is a machine-checkable statement of the envelope itself, propagated as a runtime guard rather than a compile-time comment. Then "proof holds" and "we are still inside the proof's domain" are two separate, observable properties, and the unverified-parser / unverified-runtime cases stop being invisible.

I hardly felt that the problem could be answered in such poetic and psychological eloquence. I get what you are saying.

I am building in finance, where workflows dominate - ie if A then B, but if ~ A then C then D etc. Configuration is a major challenge, but AI helps in getting there, but ever so often as you know - LLMs to the wrong thing even though they had been told many times over before. Users tend to abandon the interface and then manually make their updates. Is there a user interaction model to get the user to stay engaged ?

The other challenge that we have found is accuracy and completeness of fields required to be updated across use cases. Either we have to mandate all the fields or when we set them optional in the tool def. it sometimes blows through - how are you handling that ?