problems / neuralese-governance / enabler
authors: quinn
table stakes is that proofs are cheap. We assume a proof oracle will make code and proofs that they’re correct too cheap to meter.
One idea is that specs remain expensive, though, because we always want a human in the loop. Elicitation and validation of specs is really crucial.
But in the “specs are expensive, proofs are cheap” world, we assume some known trusted natural/human-written proof stack, like Lean or Rocq or Verus/Z3, is the substrate. What if this assumption is violated?
What if LeoGPT writes a new proof stack, where human interpretability is not a first class feature?
how do we do spec elicitation and validation then? how do we govern the proof oracle if we’ve never seen the syntax before?
TODO: flesh out.
// stack context
[execution-harness] Execution Harness
Execution Harness The execution harness is the outermost software layer of an ML deployment: the wrapper that actually calls the model and handles its inputs and outputs. A user’s prompt enters here, gets tokenized and batched, passes through the model, and returns as a completion. Because every int…
[software-framework] Software & ML Framework
Software and ML Framework Layer Between the orchestration infrastructure below and the execution harness above sits the software that actually defines and compiles a model: the frameworks researchers write against, the compilers that lower their code to GPU kernels, and the sprawling dependency grap…
[orchestration-cloud] Orchestration & Cloud
Orchestration and Cloud Layer The orchestration layer manages the compute resources that ML workloads run on: scheduling jobs across GPU clusters, routing traffic between them, and controlling who can access what. It sits below the frameworks and above the firmware — a layer of distributed systems s…