News for hackers. Stuff that matters.

A comment on Cryptol: DSL for specifying cryptographic algorithms.

Re:Cryptol: DSL for specifying cryptographic algorithms by tommd on Sunday May 24, 2015 @05:11AM (#9595749)
Some recent happenings in Cryptol land include:

  * Dylan recently released a literate Cryptol version of the CFRG's ChaCha20/Poly1305 document.  Very cool to see more Cryptol code like this.
  * Merged the fork of SBV with upstream.
  * ABC is now a supported prover.
  * Support for parallel (first to finish) proving using ':set prover=any'.
  * The type checker has been revamped for v2.3, so we should see simpler constraints "soon".
[ Parent | on HN ]
Re:Cryptol: DSL for specifying cryptographic algorithms by CHY872 on Sunday May 24, 2015 @02:59PM (#9597160)
Parallel proving should be a big bonus. Nipkow found that on the Isabelle test set, using 3 theorem proves in parallel gave as good results in 5 seconds as the best among them gave in 120.
[ Parent | on HN ]