|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | +# Valence Shell, explained without jargon |
| 6 | + |
| 7 | +*This page assumes no computing background. If you're comfortable with a |
| 8 | +command line, you may prefer [For Users](For-Users) or |
| 9 | +[For Developers](For-Developers).* |
| 10 | + |
| 11 | +--- |
| 12 | + |
| 13 | +## What is a "shell", first of all? |
| 14 | + |
| 15 | +When you use a computer, you usually click on things. Underneath the clicking, |
| 16 | +there's an older, more direct way to tell a computer what to do: you **type |
| 17 | +commands**, one line at a time — "make a folder called *taxes*", "copy this file |
| 18 | +into it", "delete that one". The program that reads those typed commands and |
| 19 | +carries them out is called a **shell**. Professionals use shells all day because |
| 20 | +typing exact instructions is fast, precise, and repeatable. |
| 21 | + |
| 22 | +The most common shells are called **bash** and **zsh**. You've been near one if |
| 23 | +you've ever seen a black window full of green or white text in a film about |
| 24 | +hackers. It's far less dramatic than that — it's just a very literal assistant. |
| 25 | + |
| 26 | +## So what's different about *this* shell? |
| 27 | + |
| 28 | +Here is the uncomfortable truth about ordinary shells: **they trust themselves.** |
| 29 | + |
| 30 | +When you tell a normal shell "delete this folder", it assumes its own delete |
| 31 | +button works. When you undo something, it *hopes* the undo puts everything back |
| 32 | +exactly as it was. Usually it does. But "usually" is doing a lot of work in that |
| 33 | +sentence, and when it's your only copy of something important, "usually" isn't |
| 34 | +good enough. |
| 35 | + |
| 36 | +Valence Shell replaces "hope" with **proof**. |
| 37 | + |
| 38 | +## What does "proof" mean here? |
| 39 | + |
| 40 | +Think about the difference between two kinds of statement: |
| 41 | + |
| 42 | +- *"I tested this bridge by driving a few trucks over it, and it held."* |
| 43 | +- *"I calculated, from the laws of physics, that this bridge holds any truck up |
| 44 | + to 40 tonnes — and here's the math, check it yourself."* |
| 45 | + |
| 46 | +The first is **testing**. It's useful, but it only tells you about the trucks |
| 47 | +you actually tried. The second is a **proof**. It covers every truck, including |
| 48 | +ones nobody has driven yet. |
| 49 | + |
| 50 | +Almost all software in the world is built the first way: tested, not proven. |
| 51 | +Valence Shell is built the second way — at least for its most important |
| 52 | +operations. The claim "undoing a *make-folder* gives you back exactly what you |
| 53 | +started with" isn't something the authors merely tried a few times. It's |
| 54 | +something they **proved mathematically**, the way you'd prove a theorem in a |
| 55 | +geometry class — except the proof is checked by a computer program that is very, |
| 56 | +very hard to fool. |
| 57 | + |
| 58 | +## Why six proofs instead of one? |
| 59 | + |
| 60 | +Valence Shell doesn't prove things once. It proves the same facts **six separate |
| 61 | +times, using six different mathematical "languages"** (they have names like Coq, |
| 62 | +Lean, and Agda — you don't need to remember them). |
| 63 | + |
| 64 | +Why the repetition? For the same reason important contracts get read by several |
| 65 | +independent lawyers. If one person makes a subtle mistake, the others are likely |
| 66 | +to catch it. If all six independent systems — built by different people, on |
| 67 | +different principles — agree that a fact is true, the chance that they *all* made |
| 68 | +the *same* mistake is vanishingly small. This "prove it several ways" approach is |
| 69 | +used for the software inside things like verified aircraft and secure government |
| 70 | +systems. |
| 71 | + |
| 72 | +## The two big ideas, in kitchen terms |
| 73 | + |
| 74 | +Valence Shell is organised around two promises: |
| 75 | + |
| 76 | +1. **"You can always undo this."** *(The proven, working part.)* |
| 77 | + Like a pencil with a perfect eraser. Made a folder by mistake? Copied the |
| 78 | + wrong file? The shell can step backwards and put the world back exactly as it |
| 79 | + was — and it can *prove* the eraser leaves no smudge. This is the part that |
| 80 | + works today. |
| 81 | + |
| 82 | +2. **"When you destroy something, it's *really* gone — and you can prove it."** |
| 83 | + *(Designed and mathematically worked out, but not yet built into the running |
| 84 | + program.)* |
| 85 | + Sometimes you *want* permanent deletion — think of the legal "right to be |
| 86 | + forgotten", where a company must genuinely erase your personal data, not just |
| 87 | + hide it. The hard part isn't deleting; it's being able to **prove to an |
| 88 | + outside inspector** that the data is truly unrecoverable. Valence Shell has |
| 89 | + the mathematics for this worked out, but has **not yet finished building it |
| 90 | + into the actual software.** |
| 91 | + |
| 92 | +The project's name for holding both promises honestly is **Mutually Assured |
| 93 | +Accountability**: both you *and* an independent checker end up with hard evidence |
| 94 | +of what really happened — nobody has to just take anybody's word for it. |
| 95 | + |
| 96 | +## Is it finished? Can I rely on it? |
| 97 | + |
| 98 | +**No, not yet — and the authors are unusually upfront about this.** |
| 99 | + |
| 100 | +- The shell **runs** and does a great deal already. |
| 101 | +- The "you can always undo this" proofs are **real and reproducible** — you can |
| 102 | + re-run them on your own computer. |
| 103 | +- But the bridge between the *proven math* and the *actual running program* is |
| 104 | + not yet fully mechanically checked — right now it's confirmed by heavy testing |
| 105 | + (roughly 85% confidence), not by an end-to-end proof. |
| 106 | +- The "provably destroyed" (right-to-be-forgotten) feature is **designed but not |
| 107 | + built yet**. |
| 108 | + |
| 109 | +So: it's a serious, honest **research prototype**, wonderful for learning, |
| 110 | +experimenting, and academic work — but **not something to trust with your only |
| 111 | +copy of anything important, and not a replacement for your everyday shell.** |
| 112 | + |
| 113 | +The project publishes its own "here's exactly what is and isn't finished" pages, |
| 114 | +which is a good sign of trustworthy engineering rather than marketing: |
| 115 | + |
| 116 | +- [Verification Status & Honest Limits](Verification-Status) |
| 117 | +- The [FAQ](https://github.com/hyperpolymath/valence-shell/blob/main/FAQ.adoc) |
| 118 | + |
| 119 | +## Why does any of this matter? |
| 120 | + |
| 121 | +Because we increasingly ask software to do things that *really* matter — handle |
| 122 | +medical records, financial transactions, legal evidence, personal data protected |
| 123 | +by law. For those jobs, "we tested it and it seemed fine" is a weak foundation. |
| 124 | +Valence Shell is part of a small but growing movement that says: for the |
| 125 | +operations that truly matter, we should be able to **prove** the software behaves |
| 126 | +— and let anyone check the proof. |
| 127 | + |
| 128 | +It's a research project exploring what that future could look like, starting with |
| 129 | +one of the oldest and most fundamental tools in computing: the humble shell. |
| 130 | + |
| 131 | +--- |
| 132 | + |
| 133 | +## Where to go next |
| 134 | + |
| 135 | +- Curious what it actually looks like to use? → [For Users](For-Users) |
| 136 | +- Want the honest "what works / what doesn't" list? → [Verification Status](Verification-Status) |
| 137 | +- Writing an article about it? → [For Marketers & Journalists](For-Marketers-and-Journalists) |
0 commit comments