3 ;;Quote: an asynchronous, triply-redundant voting system was unstable because channels sampled sensors at different times; bad at control points

3 ;;Quote: for digital flight-control use synchronous channels, sensor data to all channels, and exact-match majority voting; needs fault-tolerant clock synchronization, etc.

6 ;;Quote: formally verified Byzantine failure clock synchronization with EHDM; difficult; found many errors, though none serious

7 ;;Quote: using an interactive proof system produced a publishable proof, enumeration of all assumptions, and exploration of changed assumptions

11 ;;Quote: an automatic theorem prover may be worse; no human review and no help with discovering proof errors; should automate calculations, etc.

12 ;;Quote: need interactive system for effective theorem proving; users provide strategy and insights, computers do the calculations

12 ;;Quote: an interactive proof should produce a publishable proof and a robust, strategy for automating the proof

13 ;;Quote: a theorem prover acts as an implacable skeptic that insists on stated assumptions and justified claims; not an oracle