Reply to thread

Message: <blockquote data-quote="deaf_judger" data-source="post: 68065" data-attributes="member: 390">[PLAIN]Governed Model of Program Execution[/PLAIN]  [PLAIN]Most introductory programming courses teach execution like:  a program runs from top to bottom, performing calculations and occasionally interacting with the outside world—printing text, writing files, sending network requests.  In many languages, calculation and action are interwoven. I propose a different structure. I will seperate calculation from action and insert a governing runtime between them. The result is a deterministic, auditable model of execution implemented in Haskell. To understand the design, it is helpful to clarify two importnat ideas:  [/PLAIN]  [PLAIN]A pure function is a function that only computes a result from its inputs. It does not modify files, read from the network, print to the screen, or depend on hidden global state. Given the same inputs, it always returns the same output. In contrast, an effect (short for “side effect”) is an action that changes or observes the external world such as writing a file, sleeping for a second, or printing a line.  [/PLAIN]  [PLAIN]Most programs mix these freely. I won't. Effects will be treated as descriptions of actions of possible actions, and actually performing them will be postponed until a later, controlled stage.  [/PLAIN][PLAIN]Separating Calculation from Action[/PLAIN]  [PLAIN]My language  evaluates expressions into values. Crucially, evaluating an effect does not perform it. It produces a value that describes it.  [/PLAIN]  [PLAIN]In the evaluator:  [/PLAIN]  [CODE=haskell]  evalExpr _ (Emit ed) = Right (VEffect ed)  [/CODE]  [PLAIN]When the program encounters something like “emit this effect,” the interpreter returns a VEffect value. It does not run the effect and the interpretator remains purely computational.  After evaluation finishes, the system collects all the effect descriptions that were produced:  [/PLAIN]  [CODE=haskell]  collectEffects :: [Value] -> [EffectDescription]  collectEffects [] = []  collectEffects (VEffect ed : vs) = ed : collectEffects vs  collectEffects (VList subVs : vs) = collectEffects subVs ++ collectEffects vs  collectEffects (_ : vs) = collectEffects vs  [/CODE]  [PLAIN]This function walks through the final values of the program and extracts the list of EffectDescription structures. Everything else is ignored. At this point, the program has not changed the world. It has only described the changes it would like to make.  [/PLAIN][PLAIN]Why Treat Effects as Data?[/PLAIN]  [PLAIN]Treating effects as data provides several advantages:  [/PLAIN]  <ol> <li data-xf-list-type="ol">[PLAIN]Predictability: The interpreter is entirely deterministic. It only computes values.   [/PLAIN]  </li> <li data-xf-list-type="ol">[PLAIN]Inspectability: Before anything runs, the full set of requested actions is visible.   [/PLAIN]  </li> <li data-xf-list-type="ol">[PLAIN]Control: Another component can decide which actions should actually occur.   [/PLAIN]  </li> </ol>  [PLAIN]The system assigns each effect a unique identifier derived from its content:  [/PLAIN]  [CODE=haskell]  EffectID = SHA256(canonicalEffectBytes)  [/CODE]  [PLAIN]An effect's identity depends on what it is. If two effect descriptions are structurally identical, they have the same ID. This makes effects content-addressed. Identity is not based on when they are created or where they appear in the program. It is based solely on structure.  [/PLAIN][PLAIN]Dependency Graphs and Deterministic Scheduling[/PLAIN]  [PLAIN]Effects may depend on other effects. For example, “write to file B” might depend on “create directory A.” These dependencies are explicitly recorded. The runtime constructs a dependency graph and executes effects in layers. Effects with no unmet dependencies form a “wave” and may run in parallel:  [/PLAIN]  [CODE=haskell]  currentEntries <- mapConcurrently realizeTransition ready  return (sortOn heEffectID currentEntries ++ nextEntries)  [/CODE]  [PLAIN]All effects in a layer are executed concurrently. After execution, the results are sorted by [/PLAIN]`EffectID' [PLAIN]before being recorded. This ensures that, even though execution is parallel, the historical record is deterministic.  If some effects cannot run because their dependencies failed, they are rejected. Nothing is silently retried or implicitly reordered.   [/PLAIN][PLAIN]Authorization Before Execution[/PLAIN]  [PLAIN]Before executing an effect, the runtime checks its historical record. If an identical effect (same [/PLAIN]`EffectID'[PLAIN]) has already succeeded, it is not executed again.  [/PLAIN]  [CODE=haskell]  governorAdmit :: History -> EffectDescription -> Decision  [/CODE]  [PLAIN]If the effect has already been completed successfully, the decision is “reject.” Otherwise, it may proceed.  This guarantees idempotence. The key architectural point here is that the component deciding whether an action may occur is different from the component that knows how to perform it.  [/PLAIN][PLAIN]Executing and Verifying Effects[/PLAIN]  [PLAIN]Each type of effect has an associated specification:  [/PLAIN]  [CODE=haskell]  data EffectSpec = EffectSpec  { esRun    :: EffectDescription -> IO Outcome    ,esVerify :: EffectDescription -> IO Outcome  }  [/CODE]  [PLAIN]The runtime:  [/PLAIN]  <ul> <li data-xf-list-type="ul">[PLAIN]Decides whether the effect is allowed.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Runs it if permitted.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Verifies the result.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Records the outcome in a ledger.   [/PLAIN]  </li> </ul>[PLAIN]The Ledger[/PLAIN]  [PLAIN]Every attempted effect is appended to a persistent ledger stored in SQLite.  Each entry records:  [/PLAIN]  <ul> <li data-xf-list-type="ul">[PLAIN]The time of execution   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]The effect’s unique ID   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Its dependencies   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Whether it was admitted or rejected   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Whether it succeeded or failed   [/PLAIN]  </li> </ul>  [PLAIN]The ledger is append-only. Past entries are never modified. This creates a durable audit trail of system behavior. The system also checks for “symmetry”: identical effect IDs should not receive inconsistent admission decisions across runs. If they do, the system can detect the inconsistency.  [/PLAIN][PLAIN]Language-Level Constraints[/PLAIN]  [PLAIN]The language further enforces discipline by restricting what effect definitions may contain. Effect bodies must be simple, they cannot contain branching (if), local bindings (let), or nested functions.  For example:  [/PLAIN]  [CODE=haskell]  isControlFlow (Seq _)       = True  isControlFlow (Let _ _ _)   = True  isControlFlow (Fun _ _ _ _) = True  isControlFlow (If _ _ _)    = True  [/CODE]  [PLAIN]If an effect body includes any of these constructs, elaboration fails.This restriction ensures that effects are declarative descriptions, not mini-programs with hidden logic.  Decision-making remains in the pure computation layer or in the governing runtime.  [/PLAIN][PLAIN]Conclusion[/PLAIN]  [PLAIN]This architecture reframes program execution. Instead of:  [/PLAIN]    [PLAIN]My language enforces: :  [/PLAIN]  <ul> <li data-xf-list-type="ul">[PLAIN]Compute desired actions (purely).   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Identify and organize them.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Decide which are admissible.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Execute them in a controlled order.   [/PLAIN]  </li> <li data-xf-list-type="ul">[PLAIN]Verify and record results immutably.   [/PLAIN]  </li> </ul>  [PLAIN]The separation increases transparency and determinism. It becomes possible to inspect all intended changes before they occur. Execution history is stable and replayable. Duplicate actions are automatically suppressed.  [/PLAIN]  [PLAIN]In contrast to conventional interpreters, where IO can occur at any point in evaluation, this design introduces structure and governance.  [/PLAIN]</blockquote>

Name

Verification

Layout Options

Color Schemes

Reply to thread