3 ms·
It's kind of like, do you think it's humanly possible to correctly encode the rules of chess in, say, 6502 assembly? You probably won't do it on the first try.
by mbrock 9y ago
It's kind of like, do you think it's humanly possible to correctly encode the rules of chess in, say, 6502 assembly?
You probably won't do it on the first try. And you wouldn't immediately bet a million dollar on it. But is it possible?
Yes.
A multisig wallet shouldn't be more complicated.
Could you prove the correctness of the 6502 chess? Sure. Formal methods are not black magic. You need a semantics of the machine and a formalization of the rules.
Can you make mistakes in specifying? Yeah, duh. So combine it with peer review and throw in a bug bounty and fuzzing.
- schoen 9y agoChess is a nice example in this analogy because there are rules that people are less familiar with and might well forget about or implement incorrectly. For example, the complete castling rules are not trivial, like with the king not passing through a square currently attacked by an opposing piece https://en.wikipedia.org/wiki/Castling#Requirements https://en.wikipedia.org/wiki/Castling#Requirements and some people may neglect or misimplement en passant https://en.wikipedia.org/wiki/En_passant https://en.wikipedia.org/wiki/En_passant and the rules related to repetitive situations in the end game: https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Threefold_repetition https://en.wikipedia.org/wiki/Fifty-move_rule https://en.wikipedia.org/wiki/Fifty-move_rule (Implementing the threefold repetition rule requires maintaining historical state of a different kind than any other chess rule!) I've seen impressive hyperminimalist chess implementations that were missing these things, but that totally felt like real chess almost all of the time.
- mikeash 9y agoThere are also some really obscure rules that came about to prevent what you might call exploits. For example, it had to be clarified that you’re not allowed to castle vertically (this could happen if you promoted the king’s pawn to a rook) and that you’re not allowed to promote pawns to a piece of your opponent’s color. A perfect chess implementation from before those rule changes would no longer be correct! It’s possible to prove that code perfectly implements a formal spec. It’s tough to prove that the formal spec perfectly describes what you want it to describe.
- AstralStorm 9y agoActually easy. With any automated theorem prover you will get requests for additional proofs if any ambiguity or missing info is detected. This is a very strong if. It means the rule cannot be reduced in plain logic. The example of forward castling rule is a good one. A missing definition of some en passant situations is caught too. (E.g. situations of check.) Completely missing rule cannot be caught with these techniques. You also need to ask the prover right questions. Say: when does a chess game end. Proof requires proving the existence of a halting Oracle for any game state. Not quite easy but possible. To actually verify, you will have to provide reduction rules unless you happen to own a supercluster.
- mikeash 9y agoHow would that work? In the cases I mentioned, the rules weren’t ambiguous, they just didn’t say what most people thought they said.
- tromp 9y agoIt's relatively easy to express the rules of Go [1] in Haskell [2] [1] http://tromp.github.io/go.html http://tromp.github.io/go.html [2] http://tromp.github.io/go/SimpleGo.hs.txt http://tromp.github.io/go/SimpleGo.hs.txt