Mar 8, 2019, 6:00 PM ETConference Presentation, Keynote

A Language-Oriented System Design

Ontology System: A language-oriented permissions and configuration management system designed to be shared across different organizational systems.
Dual-Language Design: The system interfaces with users in English while maintaining an internal core based on a dependently typed language derived from type theory.
Workflow: Users submit requests for new permissions or configurations; the system identifies responsible approvers via internal queries and routes approval requests via email.
Data Synchronization: Configuration data flows out of Ontology to external systems via queries or subscriptions, while Ontology imports external data it cannot control to contextualize permissions.
Deductive Database Model: The architecture is classified as a deductive database, combining relational tables, logical inference rules, and hard-coded primitives rather than fitting purely into a relational or Prolog model.
Primitive Types: The system includes hard-coded primitive nouns (e.g., IP address ranges, port numbers) and propositions that function as base types similar to strings or integers in programming languages.

Nouns vs. Propositions: Data is categorized into "nouns" (entities like users or repositories) and "propositions" (relationships or attributes, e.g., "User A is a member of Group B").
Definition Methods: Entities are defined via three distinct methods:
- Tables (Extensional): Exhaustive enumeration of instances (e.g., a flat list of users or a table of user-group memberships).
- Rules (Intentional): Logical inference rules defining entities dynamically (e.g., "A user set is either a specific user group or a singleton user").
- Primitives: Hard-coded types that cannot be redefined within the system.
Subset Types: The system defines subsets of nouns (e.g., "traders") by combining a predicate (e.g., "may trade") with the noun, embedding proof objects directly into the data structure.
Cross-Dependencies: Definitions are not strictly hierarchical; propositions can define nouns, and nouns defined by rules can populate tables, creating complex interdependencies.

Variant and GADTs: The internal language utilizes variant types (similar to OCaml/Haskell) and Generalized Algebraic Data Types (GADTs) where constructors can return types parameterized by their arguments.
Dependent Types: The system employs dependent types where the return type of a constructor depends on the value of its arguments, enabling precise logical modeling of rules (e.g., membership in a specific singleton set).
Proof Objects: Queries and data retrieval return not just values, but "proof objects" (constants) that serve as evidence for the truth of specific propositions.
Type-Driven UI: The user interface is data-driven; users are presented only with valid options and types, ensuring all user inputs and queries are type-safe by construction.
Deletion Constraints: The type system enforces referential integrity; deleting a noun (e.g., a user group) requires the removal of all dependent proofs and references, leading to a "cascading delete" mechanism.
Trash Can Mechanism: Due to the high cost of cascading deletes, the system implements a retention period (approximately two weeks) where deleted items are moved to a "trash" rather than immediately purged.
Read Permissions: The system enforces read permissions via cascading logic; if a user lacks permission to view a primitive, all derived data referencing it is hidden from their view.

Interactive Query Construction: Users build queries by selecting templates and joining clauses (e.g., linking user groups to repository access) via a guided interface that enforces logical constraints.
Query Semantics: Queries are translated into logical formulas (e.g., Exists A, B, C, D such that...) and evaluated by the internal type checker and Prolog-like search engine.
Change Management:
- Extensional Data: Can be modified via approval workflows or by syncing with external sources (e.g., importing new users).
- Intentional Data: Cannot be directly modified by users; changes require a type upgrade/migration process where new rules replace old definitions.
English Rendering: The UI renders internal type theory constructs into natural English strings using template instantiation, prioritizing usability over perfect grammatical generation.

Undecidability Risk: The internal Prolog-like engine is Turing complete, creating a risk of infinite loops during permission resolution; the system mitigates this with abstract execution budgets.
Budget Limitations: Current execution budgets are coarse-grained; future improvements aim to specifically target recursion depth to prevent hangs without halting legitimate complex queries.
DSL Maintenance Overhead: Maintaining the custom Domain Specific Language (DSL) required re-implementing database, language, and UI components, though the underlying patterns are well-understood academic concepts.
First-Order Limitation: The system currently restricts data to first-order logic, avoiding the complexity of higher-order logic found in advanced academic research.
Extensibility: New permission types and configurations can be added simply by uploading new type declarations, allowing the core system to evolve without code upgrades.
Automated Verification: The type-driven architecture enables automated testing of policy logic, such as verifying that users can revoke their own permissions without requiring secondary approval.