2026-08-28·por Sijie Wang#cybernetics#principles

lcf-for-labor

The true category of vibe-linter. Its nodes are not behavior-specified processes (a workflow says "what happens"); they are internally stochastic — the graph only describes what counts as done + the dependency order of completion-proofs. Steps are existentially quantified: "∃ an execution that makes the validator pass." So the net is a structure of proof obligations.

The 50-year-old precedent is the LCF architecture (HOL, Isabelle): proof search is untrusted (any tactic, even neural), but thm is an abstract data type whose only constructors are the trusted kernel's inference rules. Mapping:

agent = tactic · validator = kernel inference rule · token = thm

Node semantics = a Hoare triple {hold these tokens} stochastic-blackbox {validator passes}, with fuel/timeout/escalation as the ontological semantics of failure (completion is only a hope). "The closest relative isn't Airflow, it's Isabelle — a logician went in a big circle and came back to building a proof assistant, except this time the tactic spends money."

This is also why it's a recognizer, not a generator → recognizer-not-generator.

Up: vibe-linter

sobre esta entrada

Una de las entradas de wiki de sijie. La IA en este sitio está anclada en el mismo corpus y responde en la voz de sijie, con citas que vuelven a entradas como esta — responder le cuesta dinero a sijie, así que espera detrás de un código: ingrese código de acceso →