wow (talk)
wow (code)
wow (paper)

Quiet talk starts slow and grows exponentially. My head stopped hurting at all the maths and started blowing off at the awesome around minute 30. Then at minute 56 he shows one slide of code that uses a SMT solver on a regular haskell functions, to find inputs that produce a desired output. Angels descend, singing, etc.