Formal Methods · Programming Languages · Semantics of Computation
MSc Cognitive & Decision Sciences (UCL) · MRes Art Theory & Philosophy (UAL) 19+ years experience in higher education (curriculum design, systems thinking, and interdisciplinary teaching)
My work explores how computation, data, and programming languages can be structured around equivalence rather than raw value equality.
In particular, I investigate:
-
Computation as construction: values arise from structured paths rather than primitive operations
-
Equivalence as identity: objects are defined by transformation invariants (e.g. algebraic or topological equivalence)
-
Language–database integration: programming languages paired with systems that store and query equivalence classes
This work draws on type theory, category theory, knot theory, and algebraic structures.
A family of experimental programming languages, each designed around a specific structural guarantee.
-
JtV (Julia the Viper) — explores computation as additive construction from neutral anchors (CNO), with identity defined by equivalence of construction paths
-
KRL / Tangle — a topological language where programs are braids and equivalence is isotopy; includes a mechanised core type system in Lean
-
Additional languages exploring resource constraints, real-time systems, and ethical reasoning
Database systems where identity is defined by identity, narrative, and equivalence classes rather than raw records.
-
Lithoglyph —
-
Quandle — algebraic fingerprinting using quandle invariants
-
VeriSim —
-
Other systems exploring verified and narrative-first data models
-
Mechanised proofs of type safety (Lean 4) for core language fragments
-
Dependent-type libraries in Idris2 (protocol modelling, ABI guarantees)
-
Ongoing work on equivalence-preserving transformations across systems
-
PanLL eNSAID — A Human-Things Immersive Interface (HTiI) designed as a cognitive-relief layer for neurosymbolic co-orbits. It provides a synchronous, 4-pane parallel environment (Ambient, Symbolic, Neural, World) to reduce friction and cognitive load when working with AI agents.
-
Languages: Rust, Idris2, Zig, Ephapax, Haskell, Julia, AffineScript
-
Methods: dependent types, theorem proving, property-based testing
-
Systems: reproducible builds (Guix), formally constrained FFI boundaries
I focus on small, formally grounded cores, with larger systems built around them.
My background combines:
-
cognitive science (decision-making, modelling)
-
philosophy (structure, meaning, and representation)
-
software systems (teaching, design, and implementation)
I have worked extensively in UK higher education, developing curricula and technical systems across disciplines.
This work is exploratory and research-oriented. Repositories contain a mix of:
-
formal specifications and proofs
-
prototype implementations
-
design-stage systems
Except where expressly stated, read my work as ongoing research, not finished products. All findings are tentative. All designs are provisional,
But…if you really want to know the state of anything in particular, check out my all new AFFIRMATION.adoc in the repo root directories - true to the best of my knowledge and belief as to snapshot state, according to the timestamped document. NOTE: this is a new addition to my estate, so be patient as I bring them more widely - there is a past dated example in the AffineScript repo.
Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk