Using Clojure and Overtone, Chris Ford shows how to make music starting with the basic building block of sound, the sine wave, and gradually accumulating abstractions culminating in a canon by Johann Sebastian Bach.
Functions are proofs. Um, I can see how that might work. Go on.
Types are propositions. Really? In what sense? In fact, a function is the proof of the proposition its type represents. Woah, you've lose me now.
Don't Panic! The Curry-Howard Correspondence is an elegant bridge between the planet of logic and the planet of programming, and it's not actually that hard to understand.
In this talk Chris Ford will use the Idris dependently-typed functional programming language for examples, as its type system is sophisticated enough to construct interesting automated proofs simply by writing functions. This talk is not designed to convert you into a theoretical computer scientist, but to share with you a wonderful sight in your journey through the vast and peculiar universe of programming.
Chris Ford has been fascinated by functional programming since he first encountered Haskell during a misguided attempt to study electrical engineering. He currently makes a living coding Clojure for ThoughtWorks, although he thinks that identifying with a particular programming language is like a carpenter identifying with a particular size of screwdriver.
