Michael Weber: Random Bits and Pieces

If we knew what it was we were doing, it would not be called research, would it?

Albert Einstein

via vs: Putting theory to good use: Robbing the bank with a theorem prover. The authors used the Otter proof assistant.