> I erroneously assumed that it's intended to address implementation errors (that is to replace C or asm implementations with something easier to code).
Indeed, and those are absolutely things we need to watch out for when building backends suitable for direct implementation.
> But, anyway, could you compare it somehow to the other "proving" tools that already exist, say Agda or Coq? I'm not expecting some specific information, just curious.
Agda and Coq are both much more general-purpose and powerful in terms of the types of programs and theorems they can express. Cryptol is specialized toward theorems involving functions that manipulate sequences of bits. As a result, it's much easier to start Cryptol up and prove properties of crypto algorithms, but you aren't able to express the range of theorems that you can in a dependently-typed language.
For example, Cryptol lets you write polymorphic functions and theorems, but if you wanted to prove something about such a function:
plus_id : {a} (fin a) => [a] -> Bit
plus_id x = x + 0 == x
You'd first have to instantiate `a` to some concrete size, rather than proving it for all `a`, which would be a beginner-level proof in Coq or Agda:
Main> :prove plus_id
Not a monomorphic type:
{a} (fin a) => [a] -> Bit
Main> :prove plus_id : [32] -> Bit
Q.E.D.
So overall I'd say it's the classic story of the tradeoffs of a DSL. It's easier to get up, running, and proving things within the domain, but the domain itself is more restricted.
Indeed, and those are absolutely things we need to watch out for when building backends suitable for direct implementation.
> But, anyway, could you compare it somehow to the other "proving" tools that already exist, say Agda or Coq? I'm not expecting some specific information, just curious.
Agda and Coq are both much more general-purpose and powerful in terms of the types of programs and theorems they can express. Cryptol is specialized toward theorems involving functions that manipulate sequences of bits. As a result, it's much easier to start Cryptol up and prove properties of crypto algorithms, but you aren't able to express the range of theorems that you can in a dependently-typed language.
For example, Cryptol lets you write polymorphic functions and theorems, but if you wanted to prove something about such a function:
You'd first have to instantiate `a` to some concrete size, rather than proving it for all `a`, which would be a beginner-level proof in Coq or Agda: So overall I'd say it's the classic story of the tradeoffs of a DSL. It's easier to get up, running, and proving things within the domain, but the domain itself is more restricted.