Note on Quote: Knuth on Theory vs Practice via CAUSEweb
Beware of bugs in the above code; I have only proved it correct, not tried it.
This doesn’t invalidate progress in program-proving, but something I realized while taking a course on TLA+ is that things like TLA+ can prove that a system is correct, but can’t demonstrate that a system is performant or desirable in all the other ways that the program has to operate.
Reference
-
Permalink (
2026.NTE.002) - On
- In Notes
- Tagged optimization, software-engineering
- From Quote: Knuth on Theory vs Practice
- Edit
| ← Previous | Next → |
| Tenth Physical Therapy and a little weight training 🏋️ | My Starting Point for Jekyll Themes |