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. |
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.
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.
┌─────────────────────────────────┐
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.
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)
JtV supports addition across 7 numeric domains:
| Type | Description |
|---|---|
| Machine integers |
| IEEE double-precision |
| Exact fractions (num-rational) |
| Complex numbers (num-complex) |
| Hexadecimal integer representation |
| Binary integer representation |
| Symbolic expressions (unevaluated) |
Widening follows a defined tower: Binary/Hex → Int → Float → Complex, Int → Rational.
JtV is backed by mechanised proofs:
Five libraries, all compiling cleanly under Lean 4 v4.12.0, zero sorry:
JtvCore— denotational semantics; evaluation functions; terminationJtvTheorems— algebraic properties; state independence; totalityJtvOperational— small-step + big-step semantics; progress; preservationJtvTypes— type system; purity lattice; type soundnessJtvSecurity— injection impossibility; Harvard separation guarantee; sandboxing
ABI type verification under %default total:
Language/ExprGADT enforces Data/Control distinction at the type leveldataIsNeverControltheorem: everyExpr DataLanghasisControl e = FalsePurityordering with transitivity proofNumeric tower widening (
CanWiden) with transitivity (widenTrans)
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.
JtV v2 adds reversible computation via reverse blocks:
reversible {
x += value
} -> tok // tok : ReversalToken — use-once, linear
reverse tok // undoes the block: x -= valueSnapshot-based rollback of local state
ReversalTokenis linearly typed: exactly one ofreverse tokorabandon tokSendto external handles insidereversible { }requiresirreversible { }wrapperEnables quantum-circuit simulation and Landauer-efficient computation
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.
Rust stable toolchain (
rustup)justtask runner (cargo install justor system package)Optional:
lean(for proof verification),idris2(for ABI verification)
# 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 runjtv/
├── 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| 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 |
Security is grammar, not convention — injection impossibility is structural
Show, don’t tell — formal proofs over informal claims
v1 before v2 — master the Data/Control separation before reversibility
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."
STATUS.adoc— current implementation status and proof matrixROADMAP.adoc— planned features and research directionsEXPLAINME.adoc— deep dive into the Harvard architecture and Echo type systemdocs/language/DESIGN-JTV-V2-REVERSIBILITY.md— v2 reversibility designdocs/design-decisions/0006-patacl-pivot.adoc— coprocessor ADRALIGNMENT-AFFINESCRIPT.adoc— Echo / AffineScript alignment decisionsCONTRIBUTING.adoc— how to contributeGOVERNANCE.adoc— project governance
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.