TL;DR Cryptol is an amazing tool for communicating crypto specifications with your peers, for testing crypto implementations and for doing crypto research and formal verification. It has the most amazing and practical use of a SAT solver I've ever seen.
I've touched it briefly a very long time ago, so don't believe me blindly, but this is my impression of what Cryptol is about in practice:
* If you're publishing a paper on a new cryptographic building block, lets call it AES2, you need to specify it. Instead of using the usual math-oriented pseudo-code or unreadable-to-your-peers C, you can use the Cryptol DSL, which looks familiar to your readers but can be executed and toyed with.
* If you're implementing AES2 (be it in Cryptol, C, VHDL or assembly language) you can ask the Cryptol runtime to verify it against another implementation (usually a Cryptol implementation taken from the paper on AES2, but you could write your own or use an existing implementation in another supported language). The Cryptol runtime may be able to tell you if they are mathematically identical (and I do mean mathematically: this is not unit testing but proving identity). I say "may" because not every function can be verified this way - that would solve the proven unsolvable Halting Problem. This is implemented by translating the tested implementations to logic circuits and using a SAT solver to prove that their XOR is constant 0. (Please take a moment to reflect on how awesome this is.)
* If you're researching crypto, it gives you a programming language and toolset very fit for experimenting with cryptographic building blocks and running the sorts of statistical tests that you'd want to run on them in the process of research. It also gives you tools for formal verification (mathematically proving properties of your AES2 proposal in a way that a computer can verify is error-free).
* In theory, you can compile a Cryptol specification to optimized C or VHDL and use that in your project. acfoltzer said in this thread that Cryptol 2 is a rewrite and the compiler still isn't done (it was for Cryptol 1).
In a sane world, crypto journals and standards institutes would not accept proposals of new crypto building blocks that don't come with Cryptol code, and implementations would always use the Cryptol toolset to automatically mathematically verify that their implementation is identical to the published specification, eliminating many classes of implementation bugs.
This wouldn't have prevented Heartbleed, which isn't a crypto implementation bug.
I've touched it briefly a very long time ago, so don't believe me blindly, but this is my impression of what Cryptol is about in practice:
* If you're publishing a paper on a new cryptographic building block, lets call it AES2, you need to specify it. Instead of using the usual math-oriented pseudo-code or unreadable-to-your-peers C, you can use the Cryptol DSL, which looks familiar to your readers but can be executed and toyed with.
* If you're implementing AES2 (be it in Cryptol, C, VHDL or assembly language) you can ask the Cryptol runtime to verify it against another implementation (usually a Cryptol implementation taken from the paper on AES2, but you could write your own or use an existing implementation in another supported language). The Cryptol runtime may be able to tell you if they are mathematically identical (and I do mean mathematically: this is not unit testing but proving identity). I say "may" because not every function can be verified this way - that would solve the proven unsolvable Halting Problem. This is implemented by translating the tested implementations to logic circuits and using a SAT solver to prove that their XOR is constant 0. (Please take a moment to reflect on how awesome this is.)
* If you're researching crypto, it gives you a programming language and toolset very fit for experimenting with cryptographic building blocks and running the sorts of statistical tests that you'd want to run on them in the process of research. It also gives you tools for formal verification (mathematically proving properties of your AES2 proposal in a way that a computer can verify is error-free).
* In theory, you can compile a Cryptol specification to optimized C or VHDL and use that in your project. acfoltzer said in this thread that Cryptol 2 is a rewrite and the compiler still isn't done (it was for Cryptol 1).
In a sane world, crypto journals and standards institutes would not accept proposals of new crypto building blocks that don't come with Cryptol code, and implementations would always use the Cryptol toolset to automatically mathematically verify that their implementation is identical to the published specification, eliminating many classes of implementation bugs.
This wouldn't have prevented Heartbleed, which isn't a crypto implementation bug.