Ah, sorry, I didn't mean to imply that Cryptol itself doesn't matter. It does seem very useful for its intended purpose (though again this is from an outsider's perspective).

Rather, I meant to say that you do still need to worry about what sort of code Cryptol generates if you want to address the points raised in the original article (e.g. clearing secret memory). That was my original point, anyway: Cryptol doesn't address low-level side-channel problems.

As far as integrating FaCT and Cryptol, couldn't you use Cryptol to build the reference version of a construction, then implement a fast and side-channel-resistant variant in FaCT, then use SAW to prove the two were equivalent? (Maybe not as ideal as combining the two languages, exactly, but workable.)

I really appreciate you taking the time to reply. This stuff isn't my area of expertise, obviously, but I still find it very interesting.