feat: formal task specification DSL (replace Str task descriptions) #33

Manifesto alignment

Section VIII describes "formally-specifiable languages" and "machine-checkable specifications" as required new primitives. Currently tasks are plain Str — natural language strings like "implement list.zip". This is the antithesis of the manifesto's verification-first model.

Problem

Tasks passed to agents are unstructured strings. There is no way to:

• Declare what inputs the task expects
• Express success criteria as a checkable predicate
• Constrain which effects the task may produce
• Compose tasks formally (sequence, parallel, conditional)

The agent's goal is a bag of words. Verification is impossible because there's nothing to verify against.

Design

New module: src/task_spec/spec.lex

type SuccessCriterion =
    CheckPasses(Str)           # lex_check path
  | SpecCheckPasses(Str)       # lex_spec_check on a named spec
  | TestPasses(Str)            # lex_test suite passes
  | AttestationExists(Str, Str) # fn_name, kind

type TaskSpec = {
  goal        :: Str,                    # human-readable intent (still needed)
  inputs      :: List[(Str, Str)],       # (name, type_hint) pairs
  success     :: List[SuccessCriterion], # all must hold
  allowed_effects :: List[Str],          # constrains what tools may do
}

fn is_satisfied(spec :: TaskSpec, project_root :: Str) -> [io, proc, sql] Result[Bool, Str]

TUI integration

--task flag accepts a .lex/tasks/{name}.task file (Lex literal syntax) instead of a bare string. The session records the TaskSpec and the verify step runs is_satisfied at the end.

Stretch: task composition

type TaskGraph = Atom(TaskSpec) | Seq(List[TaskGraph]) | Par(List[TaskGraph])

Acceptance

• TaskSpec type compiles and is_satisfied runs against a real project
• At least one TaskSpec in examples/ that the build agent can execute and verify
• lex check --strict src/ passes