I'm not gonna be there to fix anything that went wrong at that point.
---
I really like this analogy: assertions that are meant to always succeed are like crutches. Just like able-bodied people don't need to use crutches to walk, correctly designed programs don't need to test their own invariants to run.
Just in case: I don't mean any disrespect to people who do need crutches to walk. Nobody chooses to be disabled, but some programmers choose not to prove that their invariants hold.
> People who have an accident may become temporarily disabled, i.e., not able-bodied.
Temporarily -> no need to start over.
> And correctly-designed programs don't have “accidents”.
That's dangerously naive. Many mission critical software has bugs. That's why airplanes for example from Airbus use 'diversity' in both hardware and software. The same functionality is implemented with different sets of hardware and implemented by different teams using different programming languages. The systems are additionally designed for graceful degradation, dynamic reconfiguration, switching to alternative control software, ...
Still: Lufthansa Flight 2904 -> 'Computer logic prevented the activation of both ground spoilers and thrust reversers until a minimum compression load of at least 6.3 tons was sensed on each main landing gear strut, thus preventing the crew from achieving any braking action by the two systems before this condition was met.'
The software was surely not written in Lisp and I also would doubt they would allow Racket 'principled' macros anywhere near Flight Control Software.
> Argh, again I'm temporarily unable to make new posts, so here goes my reply.
Please don't.
You don't understand hackernews. That's a feature of this website to slow down rambling discussions. In deep discussions take your time to answer. After a certain amount of time you can reply.
It's all in the Lisp code for this website.
> What's an incorrect program going to do about its own incorrectness? Rewrite itself?
There are a lot of options:
* inform the next system to take over some functions
* remove some features, while they are faulty, until patches are loaded in
* use alternative implementations
Look at actual Flight Control Software. That's what it does and what it is designed.
Similar for other control systems, for example in power plants. They also need independent implementations controlling each other.
> Yeah, well, that's in itself precisely what's so terrible.
It's the reality. That's why mission critical systems don't believe that even verified software has no bugs.
