| |
|
|
| |
rejected by outside feedback 008): two principles, each a layer deleted because another already holds what it holds, each with one experiment that can break it before code; 1 the proof is the compiler (the verifier proves stack places and types, loop bounds, each fn's change set, no aliasing between lists, and the three executors throw it away; a C compiler must guess what Pure has proven, so verified aup should be easier to compile to C's speed than C; delete the executor as a path, the batch lanes and the AArch64 backend, emit by stitching the executor's own op bodies; break it on UAX #14: the merging the proof licenses 4x fewer instructions, no dispatch 3x less a instruction), 2 the commit is the replica (a save's extents self-delimiting and self-verifying, the link's heard their durable ack: no replication layer, the follower's files the leader's byte for byte; break it with two hosts on one Pi, cmp at sampled saves, kill -9 and open as owner; checkpoints and compaction to ship or make deterministic; the owner-choosing rule deferred); schema evolution an open question (one shape in the tree, projected on read: unmeasured, and leaves are columns); effects and screens already one boundary, backends
|
|
|
gaps as architecture and order, each hung on an invariant already there (deterministic events, the chained commit log, ordered once delivery, views as pure functions) with a first proof on the Pi, its pass number and a stop rule: 1 the computing cliff and views' fns (the slow specs all runner 2: fns send whole blocks to the executor; fns spread at load below the language, bytes as columns, fewer instructions, CALL in a view whose callees change nothing), 2 the living store's evolution (a migration a pure fn of the new module, rewritten in batches while the app answers; 030's items-wide at 1M under 5 ms unanswered, the store the same bytes), 3 distribution (committed bursts replayed by a follower, an epoch fenced owner chosen by two of three, topology as a directory app's views; two hosts on one Pi first), 4 Vega past the grid (a display list as a view type, layout in aup with text measured by the host, IME and clipboard as input events, native windows last), alongside 5 effects whose results come back as events, one entry, a C ABI v0; the app contract gathered as draft v0, the fixed limits deferred
|
