3 ms·
I was recently trying to brainstorm novel ideas to utilize theorem provers. Does anyone have any cool ideas/examples?
by blovescoffee 6y ago
I was recently trying to brainstorm novel ideas to utilize theorem provers. Does anyone have any cool ideas/examples?
- agentultra 6y agoProof-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 6y agoCan 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.