Philip Wadler - Propositions as Types (Lambda Days 2016)

I suggest a combination of theory (videos/books/papers) and practice. For practice; I highly recommend learning Haskell. If you are new to functional programming then learning Haskell is challenging and frustrating but as with any new topic the key is to not give up but keep probing. A good recent development is lot of mainstream languages are beginning to include functional paradigms such as lambda, closures etc., For example Java introduced lambda expressions, Javascript has had them for a while now. But from a first-principles stand point Haskell is as good as it gets so please do learn and code in Haskell if not at work then at least side projects. For theory I've found following material super useful. 0. This[0] is an incredibly awesome lecture where Phil Wadler takes us on a whirlwind tour of computer science. He talks us through different foundational structures on which almost everything (hardware and software) about computer science is built. I watch this lecture once every few months :-). It helps you build up context and ground various topics. 1. The one and only SICP. Book[1] and lectures[2]. 2. Automata theory[3]. This isn't an easy course but gets to the heart of the matter i.e., the meaning of "function" and what how can it be mechanically "computed". 3. Category Theory is where lot of active research is happening in CS theory. This is a very good lecture series[4]. The pace may seem a bit meandering but don't be put off. Bartosz is a gifted teacher and works i

just to note this talk briefly alludes to another subject, the Curry–Howard isomorphism, something Philip Wadler had similarly given a talk about at Lambda Days (2016) titled 'Propositions as Types'[1] (slides [2] and the video recording[3]). [1]: link [2]: link [3]: ▶ this video

> Neither is static typing. It's a layer of protection, much like tests. Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: ▶ this video Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. > I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will catch type errors in a dynamically typed language that a statically typed language picked up at compile time.. This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). A type system can reject inputs by virtue of their lack of conformance to a type, which eliminates the need to test them. > The question is whether you need to write more tests and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code. I don't have any evidence to support this (if someone does or has proof to the contrary, I'd love to see it referenced here), but I believe there is almost no overhead imposed by a static type system with type inference. > Ditto for types. I acknowledged this above, you just removed that part from the quote. In practice I've never had a bug with the type system (that I'm aware of), while I've seen hundreds of bugs from incorrect test assertions.