|
1 | | -= Julia The Viper — EXPLAINME |
2 | | -:toc: preamble |
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | += Julia the Viper — EXPLAINME |
3 | 3 |
|
4 | | -This document backs up the claims made in README with evidence and rationale. |
| 4 | +== "Harvard Architecture Language for Security-Critical Applications" |
5 | 5 |
|
6 | | -== What Is This? |
| 6 | +[quote, README] |
| 7 | +____ |
| 8 | +Julia the Viper is a Harvard Architecture programming language designed to make code injection grammatically impossible. Named after mathematician Julia Robinson (Hilbert's 10th problem) with a playful nod to "adder" (snake + addition), JtV separates computation into two grammatically distinct channels: Control Language (Turing-complete, imperative) and Data Language (Total/provably halting, addition-only). |
| 9 | +____ |
7 | 10 |
|
8 | | -Julia The Viper is a hyperpolymath project. See README.adoc for usage. |
| 11 | +The core idea is that user-supplied data can never contain control flow because the grammar physically forbids it — not through runtime validation but through separate parse grammars for Control and Data contexts. See link:docs/GRAMMAR_EVOLUTION.md[GRAMMAR_EVOLUTION.md] for the v1/v2 separation rationale and link:docs/QUANTUM_VISION.md[QUANTUM_VISION.md] for the reversible computing extension. |
9 | 12 |
|
10 | | -== Why These Choices? |
| 13 | +**Caveat:** v1 alpha is partially implemented (parser and interpreter stubs exist); the full Rust `jtv-lang` crate referenced in the README is not yet present. v2 (reversible computing) is specification-only. |
11 | 14 |
|
12 | | -=== Language |
| 15 | +=== Evidence |
13 | 16 |
|
14 | | -The language(s) used in this project were chosen per the hyperpolymath |
15 | | -language policy (see CLAUDE.md for the full list of allowed/banned languages). |
| 17 | +[cols="1,2", options="header"] |
| 18 | +|=== |
| 19 | +| Path | Proves |
16 | 20 |
|
17 | | -=== Architecture |
| 21 | +| `examples/basic/`, `examples/advanced/`, `examples/contracts/` |
| 22 | +| 17+ example programs demonstrating Control/Data separation exist |
18 | 23 |
|
19 | | -Architecture decisions are documented in `.machine_readable/` checkpoint files. |
| 24 | +| `packages/jtv-analyzer/` |
| 25 | +| Code analyzer component is present (Deno-based) |
20 | 26 |
|
21 | | -== Alternatives Considered |
| 27 | +| `fuzz/fuzz_targets/fuzz_parser.rs` |
| 28 | +| Parser fuzzing exists, confirming grammar-level enforcement approach |
22 | 29 |
|
23 | | -(To be filled in as the project matures.) |
| 30 | +| `docs/GRAMMAR_EVOLUTION.md` |
| 31 | +| v1 vs v2 grammar separation is formally documented |
24 | 32 |
|
25 | | -== Proof of Claims |
| 33 | +| `docs/QUANTUM_VISION.md` |
| 34 | +| Reversible computing / quantum simulation design is documented |
26 | 35 |
|
27 | | -(Link formal verification results from the `proven` repo where applicable.) |
| 36 | +| `packages/jtv-analyzer/abi/` |
| 37 | +| ABI definitions exist for the analyzer layer |
| 38 | +|=== |
0 commit comments