zk-SNARK/FP Talk: What does it mean to prove something?

For our first meeting, Izaak from O(1) Labs will be giving a crash course on the philosophical underpinnings of SNARKs and an OCaml DSL for using them.
———
What does it mean to prove something? Depending on who you ask, you might get one of two answers:

1. If you ask a type theorist, they'll give you an answer in something that sounds like English. They'll clarify how human concepts -- like implication, abstraction, and conjunction -- can be formally described.
2. On the other hand, if you ask a complexity theorist or cryptographer, they'll explain lots of different ways of proving something in the abstract, skipping over an explanation of what exactly it is that you're proving.

The second approach has produced amazing results, like zk-SNARKs, which are proofs of arbitrarily complex computations that fit in a few hundred bytes and can be checked in milliseconds. This approach, however, cannot stand entirely on its own: ultimately one needs a comprehensible interface to these constructions, which is essentially the domain of the first tradition.

This talk will go over these two traditions, and then explain how Snarky -- an OCaml DSL developed by O(1) Labs for writing SNARK-certified computations -- serves as such an interface bridging these two notions of proof. It should be accessible to anyone with a general background in computer science.

Snacks and refreshments will be provided.