[astrange]

Can theorem proving languages actually prove that crypto code doesn't have side channels? That kind of thing isn't in most type systems. The only project I know that has thought about is Cryptol.