Atlox

6research areas

43concepts tracked

Ideas survive by evidence.

Atlox has not followed one uninterrupted architecture plan. It has repeatedly built the smallest working model, subjected it to a harder problem, and either carried it forward or replaced it.

Research is still running, and ideas are always welcome to make a comeback.

State, transactions, and authority

8 concepts

Accepted

Abstract data types

  • Known idea. A type is defined by its operations and laws, not by one memory layout.
  • Atlox. Maps, queues, logs, signals, and other structures keep logical meaning while the runtime chooses SQL tables, indexes, brokers, replicas, or memory.
  • Current boundary. The July 25–26 data-systems work found that one function language over law-bearing structures is promising; it did not prove one universal structure.

References

Accepted

Multiversion concurrency control

  • Known idea. Retaining multiple committed versions lets readers observe a coherent snapshot while writers continue.
  • Atlox. An invocation reads one stable application snapshot. Physical revision storage remains runtime machinery rather than an application value type.
  • Current boundary. MVCC provides snapshots; it does not by itself provide serializability or an optimistic retry protocol.

References

Accepted

Optimistic concurrency control

  • Known idea. Work proceeds without holding all locks, then validates observations before commit.
  • Atlox. The runtime validates point and query observations and retries the complete invocation when a conflicting commit is still safe to rerun.
  • Current boundary. External effects with an unknown outcome cannot be hidden inside an ordinary retry.

References

Accepted

Serializability

  • Known idea. Concurrent committed operations must be equivalent to some sequential execution.
  • Atlox. Transactional application operations target serializable behavior without exposing transaction syntax in ordinary source.
  • Current boundary. Snapshot isolation alone is not enough; predicate observations and write skew must also be handled.

References

Accepted

Capability-based security

  • Known idea. Authority is represented by explicit, unforgeable rights rather than ambient global access.
  • Atlox. Storage transitions, external effects, queue claims, and physical realizers are available only through scoped capabilities.
  • Current boundary. The source surface should remain ordinary; capability detail is exposed when ownership or transfer changes observable behavior.

References

Accepted

Selective event sourcing

  • Known idea. Some state is usefully represented as a retained sequence of domain events from which current state can be reconstructed.
  • Atlox. Semantic edit history, durable workflow history, and audit ledgers can use this model. Ordinary application state does not have to become an event log.
  • Current boundary. Event sourcing is one legal realization, not the universal mutation primitive.

References

Researching

Orthogonal persistence

  • Known idea. Programs and types should not change merely because their values live briefly or survive for years; reachability from durable roots can determine retention.
  • Atlox. Functions construct ordinary values and closures. The runtime may persist their environments when rooted causal reachability, ownership, or committed obligations require it, without introducing a persistent function or allocation form.
  • Current boundary. The August 2 models validate durable owners and bounded rooted retention, but not distributed reachability, general schema evolution, offline references, or safe reclamation in production.

References

Abandoned

Exactly-once external effects

  • Known idea. “Exactly once” is often claimed for delivery, but a crash can leave a caller uncertain whether a remote side effect happened.
  • Atlox. Effects instead carry stable occurrence identity and explicit pending, succeeded, failed, or unknown outcomes.
  • Reason abandoned. No local transaction can atomically control an arbitrary remote system.

References

Incremental and temporal computation

8 concepts

Accepted

Relational algebra and logical query plans

  • Known idea. A query denotes a result independently of the physical algorithm used to produce it.
  • Atlox. Collection expressions remain values while the runtime chooses scans, joins, indexes, partitions, caches, and placement.
  • Current boundary. Physical objectives may change performance, never application-visible meaning.

References

Accepted

Incremental view maintenance

  • Known idea. A maintained result can be updated from input changes instead of recomputed from all source data.
  • Atlox. Recompute, structural deltas, indexes, caches, placement, and read-only replicas are interchangeable realizations when they agree on a pinned definition and input frontier.
  • Current boundary. Only filters have a structural delta rule in the bounded model. Joins use an index, while unsupported shapes fall back to full recomputation.

References

Accepted

Maintained ordinary functions

  • Known idea. Incremental and self-adjusting computation can update a result as its inputs change while preserving the meaning of ordinary evaluation.
  • Atlox. The same fn(A) -> B can produce Once<B> or, when admissible, Maintained<B>. Maintenance changes evaluation strategy and lifetime, not the function's logical result.
  • Current boundary. No source syntax requests maintained application yet. Effects, nondeterminism, unpinned code, transitive mutation, and cycles are rejected.

References

Researching

First-class live values

  • Known idea. A changing logical value can be observed, shared, returned, stored, and composed independently of the producer and its physical update mechanism.
  • Atlox. Experimental Live<T> values publish maintained results from exact revision-pinned reads of authoritative closure state without exposing frontiers, plans, sites, or runs.
  • Current boundary. Live<T> is not production syntax. Authority policy, offline writes, fixed points, structural collection identity, and schema migration remain unresolved.

References

Researching

Differential dataflow

  • Known idea. Collections of changes indexed by logical time support iterative, incremental, and revised computation.
  • Atlox. It is a strong candidate for recursive and revision-aware maintained computation.
  • Current boundary. Its change and time model should be adopted where required, not imposed on every scalar or transaction.

References

Accepted

Event time and watermarks

  • Known idea. Event time describes when data belongs; watermarks or progress frontiers describe how complete a time range is believed to be.
  • Atlox. Stream windows must distinguish event time, processing time, late data, and progress.
  • Current boundary. The July 25 crash test showed that an ordinary stream of values cannot preserve these distinctions.

References

Researching

The CALM theorem

  • Known idea. Monotonic programs can produce coordination-free distributed results; nonmonotonic decisions require knowledge that input is complete.
  • Atlox. The compiler can use monotonicity to explain where coordination is avoidable and where a final decision needs an authority or progress claim.
  • Current boundary. CALM is a planning law, not a complete execution model.

References

Accepted

Reactive Streams and backpressure

  • Known idea. Asynchronous producers and consumers need an explicit demand protocol and bounded mediation.
  • Atlox. A flow contract states buffering, ordering, demand, overflow, and cancellation rather than hiding them behind a generic stream.
  • Current boundary. Queue consumption, broadcast, replay, and latest-value observation remain different contracts.

References

Execution and communication

9 concepts

Researching

The actor model

  • Known idea. Independently active entities own state, receive messages, create actors, and send messages asynchronously.
  • Atlox. Mutable environments retain logical owners and may be realized as actor activations, but ordinary At source remains functions and closures rather than actor declarations.
  • Current boundary. Actor lowering is a runtime refinement. Typed causal continuity now carries stable identity across activation failure and replacement without making every relation or value a mailbox actor.

References

Accepted

Closures as the source computation kernel

  • Known idea. Closure conversion and defunctionalization can translate higher-order lexical functions into code, environment records, and first-order dispatch while preserving behavior.
  • Atlox. One typed function form covers direct calls, captured mutable state, browser-shipped computation, and functions later promoted into durable, distributed, or maintained execution.
  • Current boundary. Direct mutable capture from several independent owners and general transferable-effect analysis remain unresolved.

References

Accepted

Structured concurrency

  • Known idea. Concurrent work belongs to an explicit ownership scope that controls joining, cancellation, and failure propagation.
  • Atlox. Starting independent progress creates an owned run; child work cannot silently outlive its owner.
  • Current boundary. Long-lived services and durable workflows extend beyond finite task nurseries but retain the same ownership discipline.

References

Accepted

Durable execution

  • Known idea. An execution can persist its progress and resume after process failure without making the developer manually reconstruct every continuation.
  • Atlox. Ordinary functions lower to durable continuations and post-state deltas. Committed work resumes without replaying At code, retains definition pins, and releases mutable owners while suspended.
  • Current boundary. Real failover, multi-owner mutation, cancellation, timeout, state migration, and reclamation still require explicit protocols.

References

Accepted

Typed causal continuities

  • Known idea. Logical identity should survive replacement of the process, task, or machine that currently realizes it.
  • Atlox. A continuity is the stable subject of state, computation, or publication. Maintained evaluation can discover exact owner revisions and dependencies while consumer interests, retention, obligations, runs, and activations remain runtime realizations.
  • Current boundary. The bounded model does not yet define typed abandonment, deadline expiry, offline reconciliation, cross-owner atomicity, or state and continuation migration.

References

Researching

Algebraic effects and handlers

  • Known idea. Effectful operations can be separated from the handlers that interpret them.
  • Atlox. Installed external-function contracts now let the same ordinary function type execute pure calls, deduplicated effects, and uncertain at-most-once effects through different durable protocols.
  • Current boundary. The runtime evidence does not yet select a creator-facing algebraic-effect or handler syntax, and adapter claims still require trust or verification.

References

Researching

Session types and choreographies

  • Known idea. Communication protocols can be typed globally and projected into compatible local participant behavior.
  • Atlox. Protocol-aware structures could verify accepted inputs, possible outputs, ordering, and revision compatibility.
  • Current boundary. Research through August 2 retained typed invocation, receipt, obligation, and publication laws but has not chosen a creator-facing session-type language.

References

Researching

Linear and affine types

  • Known idea. Linear values must be used exactly once; affine values may be used at most once.
  • Atlox. These disciplines fit queue claims, leases, upload parts, and transferable capabilities that must not be duplicated.
  • Current boundary. Linearity should appear only where duplication is observably unsafe, not color every ordinary application value.

References

Abandoned

One universal data structure

  • Known idea. Abstract data types unify representation, but they do not make every protocol obey the same laws.
  • Atlox. Familiar structures share one expression language and common descriptor machinery.
  • Reason abandoned. Replacement, append, claim, merge, retraction, progress, and uncertain effects produce different legal traces.

References

Replication and delivery

5 concepts

Accepted

Conflict-free replicated data types

  • Known idea. CRDTs define merge laws that let replicas converge without central coordination.
  • Atlox. They are suitable for explicitly mergeable, independently writable state and offline collaboration.
  • Current boundary. A CRDT cannot infer domain conflict policy and is not the default for centrally authoritative transactional state.

References

Accepted

Leases and fencing tokens

  • Known idea. A time-limited lease grants temporary authority; a monotonically increasing fencing token lets resources reject stale holders.
  • Atlox. Queue claims and exclusive external work need both bounded ownership and stale-writer rejection.
  • Current boundary. A lease timeout alone is unsafe because an expired worker may still be running.

References

Accepted

Idempotency and uncertain outcomes

  • Known idea. Stable operation identity makes retries recognizable, while explicit outcome states preserve uncertainty after failures.
  • Atlox. The runtime commits one invocation identity and dispatch obligation before an effect escapes. Deduplicated adapters may retry that identity; uncertain adapters expose Unknown instead of silently repeating the effect.
  • Current boundary. Deduplication prevents duplicate meaning only when the external boundary honors its installed contract; network liveness and adapter verification remain open.

References

Accepted

Transactional outbox

  • Known idea. A database change and an outgoing message intention are committed together, then a relay performs delivery.
  • Atlox. Atomic turns commit state, caller continuation, and an external dispatch obligation together without pretending the remote effect shares the Atlox database transaction.
  • Current boundary. Delivery and remote acceptance remain separate observable facts.

References

Accepted

Snapshot-plus-log handoff

  • Known idea. A consumer obtains a coherent snapshot and then continues from an ordered change position without a gap.
  • Atlox. Browser replicas and maintained observations use snapshot state plus a checkpointed change stream.
  • Current boundary. Resume requires retained, ordered changes or a new snapshot when history is no longer available.

References

Semantic programs and evolution

6 concepts

Returned

Projectional editing

  • Known idea. A projectional editor modifies the program model directly and renders source-like views instead of treating text as the source of truth.
  • Atlox. Semantic commands preserve definition identity, make refactorings atomic, and keep invalid drafts separate from the accepted program.
  • Current boundary. The editor must retain normal text-editing ergonomics without accepting arbitrary structure-breaking replacement.

References

Accepted

Stable semantic identity

  • Known idea. Content-addressed and model-based systems separate a definition’s identity from its current name or file location.
  • Atlox. Records, fields, functions, files, runs, and deployed revisions keep stable identities across relabeling and movement.
  • Current boundary. Meaning-changing replacement must create a new identity rather than disguise itself as a rename.

References

Researching

Bidirectional transformations and lenses

  • Known idea. A lens relates a source and a view through forward and backward transformations constrained by round-trip laws.
  • Atlox. Lenses may help update record views and transport compatible state across program revisions.
  • Current boundary. Arbitrary splits, information loss, and concurrent old/new writes cannot be solved by a generated inverse.

References

Accepted

Expand-and-contract evolution

  • Known idea. Systems first add a compatible representation, move traffic and data, then retire the old representation.
  • Atlox. Deployment plans can generate coexistence, backfill, activation, rollback, and reclamation after the developer resolves semantic ambiguity.
  • Current boundary. The technique automates mechanics, not missing domain information.

References

Accepted

Multiversion code and protocol coexistence

  • Known idea. Immutable code revisions can remain available while old executions and clients still depend on them.
  • Atlox. Active runs stay pinned to the revision they started with while deployment activates a newer revision for new work.
  • Current boundary. Automatic transport is allowed only when recorded semantic operations prove compatibility.

References

Accepted

Operation-based model evolution

  • Known idea. An operation log records how a model changed, preserving intent that a final snapshot cannot recover.
  • Atlox. Create, relabel, move, split, merge, retire, and replace are semantic operations that drive diagnostics and deployment planning.
  • Current boundary. The log captures structural intent; domain transformations still require localized creator decisions.

References

Formal semantics and verification

7 concepts

Researching

Structural operational semantics

  • Known idea. A language can be defined by syntax-directed transition rules over explicit configurations.
  • Atlox. Recent function, durability, effect, and continuity slices each define explicit transitions and execute them in independent bounded reference models.
  • Current boundary. One generic transition machine can encode many systems while erasing the algebra needed for useful analysis.

References

Accepted

Labelled transition systems

  • Known idea. States and labelled transitions provide a neutral way to compare observable behavior and generate counterexamples.
  • Atlox. Research candidates are normalized to bounded traces to test safety, retry, ordering, cancellation, and coexistence claims.
  • Current boundary. Matching bounded traces is evidence, not a proof of contextual equivalence or liveness.

References

Researching

Trace refinement

  • Known idea. An implementation refines a specification when every relevant implementation behavior is permitted by the specification.
  • Atlox. Physical realizers should justify that SQL, queues, browser replicas, and workflows preserve the source contract.
  • Current boundary. Research through August 2 compares direct, converted, durable, and failure-injected executions, but it has not produced production realizer proofs.

References

Researching

Institution theory

  • Known idea. Institutions describe signatures, models, sentences, satisfaction, and satisfaction-preserving translations independently of one particular logic.
  • Atlox. The July 27 meta-runtime research uses this as a candidate framework for relating database, process, protocol, dataflow, and transaction theories.
  • Current boundary. It organizes heterogeneous theories; it does not itself provide executable computation or physical planning.

References

Researching

Unifying Theories of Programming

  • Known idea. UTP characterizes programming paradigms through observable variables, healthiness conditions, laws, and refinement.
  • Atlox. It is a candidate way to state which observations each semantic region preserves while allowing checked links between regions.
  • Current boundary. Its adequacy for databases, incremental progress, security, and program evolution still has to be demonstrated.

References

Accepted

Property-based testing

  • Known idea. Generators explore many inputs while properties and shrinking expose minimal counterexamples.
  • Atlox. Parser, runtime, evolution, and incremental paths are tested against laws rather than only curated examples.
  • Current boundary. Passing generated tests increases confidence; it does not prove the law.

References

Accepted

Bounded model checking

  • Known idea. A finite state space can be exhaustively searched for safety violations and short counterexamples.
  • Atlox. Recent research compares good models with deliberately broken mutants, injects crashes around commit boundaries, and records the exact state, transition, and scenario bounds.
  • Current boundary. Bounded safety does not establish unbounded safety, liveness, fairness, or production conformance.

References