Couldn’t agree more. I am a current (mid career) PhD student in cryptography and WOW is it a mess. Provable security arguments are generally written in the impl

Couldn’t agree more. I am a current (mid career) PhD student in cryptography and WOW is it a mess. Provable security arguments are generally written in the implicit propositional logic + set theory of working mathematicians, but it is woefully inadequate for the job. Some very powerful composable frameworks have been developed, but they are really straining against the clunkiness of the formal system in which they have been constructed. The best new ideas I’ve seen for formalizing cryptographic settings all belong in category theory or topology, but have been formalized in set theory because that seems to be the only tool that the average cryptographer intuitively knows how to use.