Skip to content

Commit af1fef6

Browse files
hyperpolymathhyperpolymath
authored
Update README.adoc
1 parent 0055db7 commit af1fef6

1 file changed

Lines changed: 320 additions & 1 deletion

File tree

‎README.adoc‎

Lines changed: 320 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,326 @@ image:https://img.shields.io/badge/Philosophy-Palimpsest-indigo.svg[Palimpsest,l
66

77
:toc: left
88
:toclevels: 3
9-
:icons: font
9+
:icons: font= Julia the Viper (JtV)
10+
:toc:
11+
:toclevels: 2
12+
:sectnums:
13+
14+
Julia the Viper (JtV) is a stratified programming language project centered on a strict separation between a restricted *Data* fragment and a general *Control* fragment.
15+
16+
Its central design aim is simple:
17+
18+
____
19+
make certain classes of control/data confusion structurally unavailable, rather than merely discouraged by convention.
20+
____
21+
22+
JtV is implemented in Rust, supported by a growing proof and testing stack, and documented in AsciiDoc as the canonical format for repository documentation.
23+
24+
== Current Status
25+
26+
JtV is *not* “finished”, “100% complete”, or “fully verified end-to-end”.
27+
28+
It *is*:
29+
30+
- an implemented core language project
31+
- substantially tested
32+
- partially mechanised
33+
- supported by a growing formal and academic documentation set
34+
- surrounded by several planned extensions that are *not yet part of the stable core*
35+
36+
The best current summary is:
37+
38+
____
39+
JtV has a real implemented and tested core, with partial formalisation and a larger speculative halo of future features.
40+
____
41+
42+
For the most accurate current state, see:
43+
44+
- `STATUS.adoc` or `STATUS.md` if still transitional
45+
- `TEST-NEEDS.md`
46+
- `ROADMAP.adoc`
47+
48+
== Core Idea
49+
50+
JtV separates computation into two distinct regions:
51+
52+
=== Data Fragment
53+
54+
The Data fragment is intended to be:
55+
56+
- restricted
57+
- side-effect-free
58+
- easier to reason about
59+
- structurally separated from general control flow
60+
61+
In the current design direction, Data expressions exclude constructs such as:
62+
63+
- loops
64+
- general control statements
65+
- assignments
66+
- unrestricted effectful computation
67+
68+
This is the main architectural idea behind the project.
69+
70+
=== Control Fragment
71+
72+
The Control fragment is the general execution layer. It is intended to handle:
73+
74+
- sequencing
75+
- branching
76+
- iteration
77+
- state changes
78+
- I/O
79+
- runtime orchestration
80+
81+
The Data fragment may be embedded in Control, but the reverse is deliberately restricted.
82+
83+
== Why This Exists
84+
85+
Traditional systems often rely on runtime discipline to keep data from becoming executable control.
86+
87+
JtV explores a different route:
88+
89+
- separate the fragments in syntax
90+
- reinforce the split in typing and effects
91+
- make the boundary explicit in implementation and tests
92+
- reason about the restricted fragment more strongly than the unrestricted one
93+
94+
This does *not* magically solve every security problem.
95+
96+
It does, however, create a clearer foundation for reasoning about:
97+
98+
- restricted computation
99+
- purity
100+
- totality of a core fragment
101+
- reversible sub-fragments
102+
- language-level control/data discipline
103+
104+
== Current Project Scope
105+
106+
=== What Is Part of the Current Core
107+
108+
The current defensible core includes, at minimum:
109+
110+
- parser and grammar work
111+
- Rust interpreter core
112+
- Data / Control separation as a first-class project idea
113+
- multiple numeric forms
114+
- property tests, fuzz targets, and contract tests
115+
- proof artifacts for parts of the core
116+
- early reversible-computation support in a constrained fragment
117+
118+
=== What Is *Not* Yet Stable Core
119+
120+
The following are documented, explored, or partially specified, but should be treated as extensions or research directions unless explicitly marked otherwise:
121+
122+
- refinement types
123+
- dependent types
124+
- linear / affine types
125+
- effect polymorphism
126+
- full type-class machinery
127+
- gradual typing
128+
- sized types
129+
- full symbolic simplification
130+
- probabilistic extensions
131+
- quantum algorithm libraries
132+
- full end-to-end verification chain
133+
134+
== Reversibility
135+
136+
Reversibility is an important theme in JtV, but it must be stated precisely.
137+
138+
At present, the strongest technical sense of reversibility in JtV is:
139+
140+
- a restricted reversible computational fragment
141+
- based on constrained invertible updates
142+
- supported by tests and ongoing semantic clarification
143+
144+
JtV does *not* yet justify broad claims like “full quantum language” or “thermodynamically efficient computation” as current implementation facts.
145+
146+
Those belong, where appropriate, to:
147+
148+
- future work
149+
- theoretical motivation
150+
- or extension documents
151+
152+
See:
153+
154+
- `REVERSIBILITY.adoc` if present
155+
- `docs/reversibility/`
156+
- `academic/`
157+
- `jtv_proofs/`
158+
159+
== Repository Structure
160+
161+
The repository is organized around implementation, proofs, specs, and documentation.
162+
163+
Typical key areas include:
164+
165+
- `crates/` — Rust crates for the language and tooling
166+
- `shared/grammar/` — grammar artifacts
167+
- `jtv_proofs/` — Lean proof artifacts
168+
- `academic/` — academic and formal documentation
169+
- `spec/` — language and design specifications
170+
- `verification/` — verification-related materials
171+
- `fuzz/` — fuzzing targets
172+
- `conformance/` — conformance material
173+
- `ffi/zig/` — Zig FFI work
174+
- `vscode-extension/` — editor integration
175+
- `playground/` / `web/` — web-facing tooling and experimentation
176+
177+
== Build and Development
178+
179+
JtV uses `just` for common development workflows.
180+
181+
Common commands include:
182+
183+
[source,bash]
184+
----
185+
just --list
186+
just build
187+
just test
188+
just smoke
189+
just doctor
190+
just bench
191+
----
192+
193+
You can also use Cargo directly for core testing:
194+
195+
[source,bash]
196+
----
197+
cargo test -p jtv-core
198+
----
199+
200+
Useful targeted commands may include:
201+
202+
[source,bash]
203+
----
204+
cargo test --test property_tests
205+
cargo test --test harvard_boundary_tests
206+
cargo test --test contract_tests
207+
cargo +nightly fuzz run fuzz_parser
208+
----
209+
210+
If you use Nix:
211+
212+
[source,bash]
213+
----
214+
nix develop
215+
nix build
216+
----
217+
218+
== Testing and Verification
219+
220+
JtV’s current strength is increasingly in the implemented/tested core, not just in design prose.
221+
222+
The repository includes evidence such as:
223+
224+
- inline unit tests
225+
- parser and grammar tests
226+
- property-based tests
227+
- Harvard-boundary tests
228+
- contract / invariant tests
229+
- conformance tests
230+
- fuzz targets
231+
- benchmark suites
232+
- proof-regression workflows
233+
- Lean and Idris artifacts
234+
235+
This does *not* mean every language-level or white-paper-level claim is already fully verified.
236+
237+
It *does* mean the core is much more grounded than a purely speculative prototype.
238+
239+
See:
240+
241+
- `TEST-NEEDS.md`
242+
- `READINESS.md` if retained
243+
- proof CI and verification directories
244+
245+
== Documentation Policy
246+
247+
AsciiDoc is the canonical documentation format for this repository.
248+
249+
If Markdown files remain, they should be treated as:
250+
251+
- transitional
252+
- stubs
253+
- or compatibility files only
254+
255+
If both `.md` and `.adoc` versions of a document exist, the `.adoc` version is authoritative.
256+
257+
== What To Read Next
258+
259+
For different purposes:
260+
261+
=== To understand the current project
262+
- `STATUS.adoc`
263+
- `ROADMAP.adoc`
264+
- `TEST-NEEDS.md`
265+
266+
=== To understand the language direction
267+
- `shared/grammar/`
268+
- `spec/`
269+
- `docs/language/` if present
270+
271+
=== To understand the formal / academic side
272+
- `academic/`
273+
- `jtv_proofs/`
274+
- `verification/`
275+
276+
=== To contribute
277+
- `CONTRIBUTING.adoc`
278+
- `DEVELOPMENT_PLAN.md` or its replacement if still retained
279+
- `Justfile`
280+
281+
== Contribution and Governance
282+
283+
JtV is an active project, not a frozen release artifact.
284+
285+
Contributions should be guided by:
286+
287+
- current implementation reality
288+
- explicit status documents
289+
- the distinction between stable core and speculative extension work
290+
291+
Please consult:
292+
293+
- `CONTRIBUTING.adoc`
294+
- `CODE_OF_CONDUCT.adoc` or `CODE_OF_CONDUCT.md`
295+
- `GOVERNANCE.adoc`
296+
- `SECURITY.adoc` or `SECURITY.md`
297+
298+
== Licensing
299+
300+
Refer to the repository licensing files for the current authoritative licensing arrangement:
301+
302+
- `LICENSE`
303+
- `LICENSING.md`
304+
- any additional project license files in root
305+
306+
Do not rely on older duplicated readmes for licensing summaries.
307+
308+
== Name
309+
310+
“Julia the Viper” is both a serious and playful name.
311+
312+
It gestures toward:
313+
314+
- Julia Robinson
315+
- the “adder” / snake / calculator wordplay
316+
- the project’s emphasis on addition-centered restricted computation
317+
318+
The name is part of the project’s character, but the language should be judged by the clarity of its semantics, implementation, and proofs.
319+
320+
== Bottom Line
321+
322+
JtV is best understood today as:
323+
324+
____
325+
a language project with a strong central architectural idea, a real and increasingly well-tested implementation core, partial formalisation, and a large set of ambitious extensions that still need disciplined separation from the stable core.
326+
____
327+
328+
That is a good place to be — provided the documentation remains honest about where the core ends and the research programme begins.
10329
:source-highlighter: rouge
11330
:experimental:
12331

0 commit comments

Comments
 (0)