[agentultra]

Proof-carrying code is an interesting area for privacy and security. It would be nice to know that your differential privacy algorithm doesn't leak private information or that your hashing algorithm doesn't expose side channels. Being able to keep the spec in line with the compiled code, so called deep spec, work is super dope.

[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.