Tim quoth: |> I was reading the logic programming/theorem proving chapter of my new |> Russell and Norvig book on AI, and came across something I once knew about |> but had forgotten: the Boyer-Moore theorem prover was applied to the RSA |> algorithm and the correctness of it was verified. Correctness in the sense |> of showing that outputs match formal specs, for all inputs. |> The paper is: Boyer, R.S and Moore, J.S. (1984). Proof checking the RSA |> public key encryption algorithm, "American Mathematical Monthly," |> 91(3):181-189. Given the enormous difficulty of ensuring security in a world of ubiquitous distributed computing, I'm as big a fan as any of formal methods. But Tim's post hammers home the big fault of formal methods: the possibility that people will come to rely upon them. I have paranoid visions of people finally accepting formal methods in a decade or so, and then becoming dependent on them... forgeting the enormous potential for error that will always exist in such systems. If somebody told me that intentionally letting a few violent criminals free each year is a good idea because it would keep me on my toes, I would think that person is an idiot. But I'm not entirely convinced that it is a bad idea to avoid formal methods because they could breed complacency. Cheers, JWS