Josh

Building in the open

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.

Keyboard Shortcuts

Key Action
o Source
e Edit
i Insight
r Random
h Home
s or / Search
Josh Beckman: https://www.joshbeckman.org/notes/975169493