Ok, yeah, we're on same page now. Far as Cryptol, I wanted to seeif it could be extended to generate FaCT which generated constant-time code. It would also gene

Ok, yeah, we're on same page now. Far as Cryptol, I wanted to seeif it could be extended to generate FaCT which generated constant-time code. It would also generate C to check with SAW or other tools for extra checking or situations where side channels didn't matter. Could also be a tool that checked equivalence of the two at source or object code level so any checking of C code applied to FaCT. That should cover most of the problem areas. I still think C itself or SPARK Ada could be modified to do what FaCT does. Some subset at least. Then, one can eliminate need to build FaCT-based tooling. So, those were the ideas I was brainstorming at least for what applies directly to those languages.