Introduce

http://cryptol.net/
https://github.com/GaloisInc/cryptol 

Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language.

SHA1 implemention

f : ([8], [32], [32], [32]) -> [32]
f (t, x, y, z) =
  if (0 <= t)  && (t <= 19) then (x && y) ^ (~x && z)
   | (20 <= t) && (t <= 39) then x ^ y ^ z
   | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
   | (60 <= t) && (t <= 79) then x ^ y ^ z
   else error "f: t out of range"