On Tue, 12 May 2015, Paul Rubin wrote:

> Stefan.Lucks@uni-weimar.de writes:
>>   pre => (for I in 2 .. N-1 => (N mod I /=0))
>
> Of course that still doesn't prove that N is prime: you need a separate
> proof that N has no divisors greater than N, and that proof has to
> quantify over all the integers, so it's not executable at all.  Stuff
> like this is why formal methods are often less convenient than we'd
> like.

Good Point!

------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--