Quite nice, but how about the need for key functions to be constant-time to thwart time-based attacks? It's probably quite hard to express and requires low-level per-platform tweaking.
I wrote the paper mostly in the context of implementing signature verification, which doesn't require side-channel protection since there are no secrets in verification. But, I think the DSL approach is even more important for ECDH and signing, where side-channel protection is important.
Finally, given that processors don't even promise us that any instruction is constant-time, and given that other types of attacks are possible where constant-timesness doesn't help so much (e.g. power analysis), I think it is worth considering other approaches to side-channel protection (e.g. blinding). For many applications, constant-timeness isn't sufficient and I'd love to learn that it isn't necessary.
One project that tries to do something like this is Nadeko: https://www.reddit.com/r/rust/comments/3696wt/checking_that_...