provide an ideal teaching tool because they bridge the gap between theoretical
mathematics and practical computer science), but have been limited in
their practical use to assuring the correctness of cryptographic algorithms
and security protocols, and of small high-consequence software programs,