Julia the Viper (JtV)

A research programming language exploring structured separation of data and control, and computation as constrained construction.

---

Overview

Julia the Viper (JtV) is an experimental programming language built around a simple architectural idea:

separate data and control at the level of syntax and semantics, not just convention.

The language is structured as two distinct fragments:

• Data: restricted, side-effect-free expressions

• Control: general computation (loops, branching, state, I/O)

The goal is not to eliminate all classes of error, but to make certain forms of control/data confusion structurally unavailable.

---

Current Status

JtV is an active research project, not a finished or fully verified system.

At present it includes:

• an implemented Rust-based core

• a defined (and evolving) grammar

• a substantial test suite (unit, property, fuzz, contract)

• partial formalisation (Lean and Idris artifacts)

• documentation of both implemented features and research directions

It is best understood as:

a working core language with tests and partial formal grounding, surrounded by a larger set of experimental extensions.

For current details, see:

• STATUS.adoc

• TEST-NEEDS.md

• ROADMAP.adoc

---

Core Idea

Data Fragment

The Data fragment is intentionally restricted:

• no loops or general control flow

• no side effects

• limited forms of expression (currently centred on additive construction)

This fragment is designed to be:

• easier to reason about

• closer to total or terminating computation

• structurally separated from execution logic

---

Control Fragment

The Control fragment provides general computation:

• sequencing, branching, iteration

• state updates and I/O

• orchestration of program execution

Data expressions can be embedded within Control, but not vice versa.

---

Design Direction

A key direction of the project is:

computation via construction from neutral anchors (CNO), rather than primitive destructive operations.

In this view:

• addition represents construction

• inversion (where defined) represents undoing construction, not primitive subtraction

• identity depends on how values are constructed, not just their final form

This perspective is still under active development and should be read as part of the research direction rather than a fully stabilised feature set.

---

Reversibility (Current vs Planned)

Reversibility is an important theme, but its current status is limited.

Currently

• constrained reversible behaviour in restricted fragments

• property tests exploring round-trip behaviour

Not Yet Implemented

• general reversible execution

• full semantic model of inversion across all constructs

• quantum or thermodynamic interpretations

These belong to future work, not current guarantees.

See REVERSIBILITY.adoc for details.

---

Scope

Stable / Defensible Core

• parser and grammar work

• Rust interpreter core

• explicit Data vs Control separation

• multi-type numeric support

• test infrastructure (property, fuzz, contract)

• initial proof artifacts

---

Research / Experimental Areas

The following are not part of the stable core:

• dependent or refinement types

• advanced effect systems

• probabilistic or quantum extensions

• full symbolic reasoning

• complete end-to-end verification chain

They are documented as research directions, not current features.

---

Repository Structure (Overview)

• crates/ — Rust implementation

• shared/grammar/ — grammar artifacts

• spec/ — language specifications

• jtv_proofs/ — formal proofs (Lean/Idris)

• verification/ — verification materials

• conformance/, fuzz/ — testing infrastructure

• docs/, academic/ — documentation

---

Development

Common commands:

---

just build just test just doctor

Or via Cargo:

---

## cargo test -p jtv-core

Nix is supported for reproducible builds.

---

== Documentation Policy

AsciiDoc (`.adoc`) is the canonical format.

Markdown files, where present, are transitional or secondary.

---

== How to Read This Repository

If you are new:

1. Start with this README
2. See `STATUS.adoc` and `ROADMAP.adoc`
3. Explore `spec/` and `shared/grammar/`
4. Review tests and proof artifacts for grounding

---

== Summary

JtV is best understood as:

> a language with a clear architectural idea, an implemented and tested core, partial formalisation, and an active research programme around constrained computation and equivalence-based reasoning.