JtV

A Harvard-architecture programming language that makes code injection grammatically impossible — not as a runtime check, but as a structural guarantee.

Named after mathematician Julia Robinson (Hilbert’s 10th problem) with a playful nod to "adder": a snake, and the fundamental operation the language builds everything from.

Note	Formerly "Julia the Viper". The project now goes by JtV so the "Julia" in the name is no longer mistaken — by people and bots alike — for the Julia programming language. The Julia-Robinson honour and the "adder" pun carry over to the short name.

---

The One-Line Idea

Separate Data (total, addition-only) from Control (Turing-complete, imperative) at the grammar level. Then code injection becomes an ill-formed sentence, not a runtime error.

---

Why This Matters

Code injection attacks — SQL injection, shell injection, template injection — all share the same root cause: user-controlled data reaches a context that interprets it as code. Filters, escaping, and sandboxes are defence by convention. They fail.

JtV makes the failure mode structurally impossible:

• The Data Language grammar cannot express control constructs. No if. No loops. No function calls to impure code. Only addition-based construction.

• The Control Language can embed Data expressions but not vice versa.

• A parser for Data will reject control constructs before they reach any evaluator.

This is security by grammatical impossibility, not security by convention.

---

Architecture

Harvard Separation

                 ┌─────────────────────────────────┐
User Input ────► │  DATA LANGUAGE                  │
                 │  (Total, addition-only, halting) │
                 └──────────────┬──────────────────┘
                                │ values only
                 ┌──────────────▼──────────────────┐
                 │  CONTROL LANGUAGE                │
                 │  (Turing-complete, imperative)   │
                 └─────────────────────────────────┘

The arrow is one-way. Data results flow up into Control variables. Control constructs cannot appear inside Data expressions. The grammar enforces this structurally.

Data Language

The Data fragment is intentionally restricted:

• No loops or general control flow

• No side effects or I/O

• One binary operation: addition (across 7 number systems)

• Unary negation — subtraction is a + (-b)

• Provably terminating (total by construction)

Control Language

The Control fragment provides general computation:

• Assignment, sequencing, branching (if/else), iteration (while)

• I/O and state updates

• Calls to pure data functions

• Reversible blocks (reversible { } → tok, v2)

---

Number Systems

JtV supports addition across 7 numeric domains:

Type	Description
Int	Machine integers
Float	IEEE double-precision
Rational	Exact fractions (num-rational)
Complex	Complex numbers (num-complex)
Hex	Hexadecimal integer representation
Binary	Binary integer representation
Symbolic	Symbolic expressions (unevaluated)

Widening follows a defined tower: Binary/Hex → Int → Float → Complex, Int → Rational.

---

Formal Verification

JtV is backed by mechanised proofs:

Lean 4 (jtv_proofs/)

Five libraries, all compiling cleanly under Lean 4 v4.12.0, zero sorry:

• JtvCore — denotational semantics; evaluation functions; termination

• JtvTheorems — algebraic properties; state independence; totality

• JtvOperational — small-step + big-step semantics; progress; preservation

• JtvTypes — type system; purity lattice; type soundness

• JtvSecurity — injection impossibility; Harvard separation guarantee; sandboxing

Idris2 (src/abi/Types.idr)

ABI type verification under %default total:

• Language / Expr GADT enforces Data/Control distinction at the type level

• dataIsNeverControl theorem: every Expr DataLang has isControl e = False

• Purity ordering with transitivity proof

• Numeric tower widening (CanWiden) with transitivity (widenTrans)

Echo Type System (jtv_proofs/JtvEcho.lean)

Phase 2 mechanisation of the Echo effect dimension:

• Three echo classes: EchoSafe (injective), EchoNeutral (residue retained), EchoBreaking (total erasure)

• Retained-loss lineage fibre: Echo f y := Σ x, f x = y

• @echo(safe|neutral|breaking) annotation semantics

---

Echo Type System

Echo is an effect dimension, not a value type. It tracks what information is preserved through a computation:

• @echo(safe) — bijective; full round-trip possible

• @echo(neutral) — lossy, but the residue is retained and available for audit

• @echo(breaking) — total erasure; no lineage recovery

Numeric conversions follow the 3-way rule: * Exact (e.g. Int→Rational): Safe * Lossy with residue (e.g. Float→Int, carries truncation residue): Neutral * Lossy without residue (e.g. Int→Bool, drops all but sign): Breaking

See ALIGNMENT-AFFINESCRIPT.adoc for the full design rationale.

---

v2 Reversibility

JtV v2 adds reversible computation via reverse blocks:

reversible {
    x += value
} -> tok          // tok : ReversalToken — use-once, linear

reverse tok       // undoes the block: x -= value

• Snapshot-based rollback of local state

• ReversalToken is linearly typed: exactly one of reverse tok or abandon tok

• Send to external handles inside reversible { } requires irreversible { } wrapper

• Enables quantum-circuit simulation and Landauer-efficient computation

---

Coprocessor Support (PataCL Integration)

Post-pivot 2026-04-19: compile-time decisions are delegated to PataCL, a sibling decision language:

extern coproc riscv_ext {
    gate_name: "jtv:riscv:v-ext"
}

JtV references PataCL gates by identifier. PataCL evaluates target predicates and returns liveness + family strings. JtV’s grammar does not embed predicate syntax (ADR-0006).

Current status: design complete; implementation gated on PataCL Phase 1.

---

Building

Prerequisites

• Rust stable toolchain (rustup)

• just task runner (cargo install just or system package)

• Optional: lean (for proof verification), idris2 (for ABI verification)

Quick Start

# Build the core crate
just build

# Run the full test suite (531 tests)
just test

# Run only jtv-core tests
cargo test -p jtv-core

# Check formal proofs (requires Lean 4)
cd jtv_proofs && lake build

# Check ABI types (requires Idris2)
cd src/abi && idris2 --check Types.idr

# Run REPL
just run

WASM

just build-wasm   # requires wasm-pack

---

Repository Structure

jtv/
├── crates/
│   ├── jtv-core/         Rust interpreter + type system + reversibility
│   ├── jtv-cli/          REPL and command-line interface
│   ├── jtv-lsp/          LSP server (tower-lsp)
│   └── jtv-debug/        Debug adapter
├── jtv_proofs/           Lean 4 formal proofs (5 libraries)
├── src/abi/              Idris2 ABI type verification
├── spec/                 Language specifications (EBNF, type system)
├── docs/                 Design decisions (ADRs), language docs
├── fuzz/                 Cargo fuzz targets
├── conformance/          Conformance test corpus
├── .machine_readable/    Machine-readable project metadata (A2ML)
└── .github/workflows/    CI pipelines

---

CI Status

Check	Status
Lean 4 proof regression	✅ Passing
Idris2 ABI verification	✅ Passing
Rust (build, test, clippy, fmt)	✅ Passing
Governance (language policy, security, linting)	✅ Passing
Hypatia neurosymbolic scan	✅ Passing
ClusterFuzzLite (address, undefined sanitizer)	✅ Configured

---

Project Philosophy

1. Security is grammar, not convention — injection impossibility is structural

2. Show, don’t tell — formal proofs over informal claims

3. v1 before v2 — master the Data/Control separation before reversibility

4. Accessibility first — all tooling supports --help, plain-text output, no colour-only signalling

Named after Julia Robinson (1919–1985), who proved that Hilbert’s 10th problem is undecidable. The "Viper" is a snake — an adder — fitting for a language whose Data fragment is built entirely from addition.

"It’s basically the same thing as an adder."

---

Further Reading

• STATUS.adoc — current implementation status and proof matrix

• ROADMAP.adoc — planned features and research directions

• EXPLAINME.adoc — deep dive into the Harvard architecture and Echo type system

• docs/language/DESIGN-JTV-V2-REVERSIBILITY.md — v2 reversibility design

• docs/design-decisions/0006-patacl-pivot.adoc — coprocessor ADR

• ALIGNMENT-AFFINESCRIPT.adoc — Echo / AffineScript alignment decisions

• CONTRIBUTING.adoc — how to contribute

• GOVERNANCE.adoc — project governance

---

Licence

Dual-licensed by artifact type: source code under MPL-2.0 (Mozilla Public License 2.0); documentation under CC-BY-SA-4.0. See LICENSING.md for details.