Type-Driven Development in Idris - Edwin Brady

Idris is a general purpose pure functional programming language with dependent types. In Idris, types are a first class language construct, meaning that they can be manipulated and computed like any other language construct. It encourages a type-driven style of development, in which programmers give types first and use interactive editing tools to derive programs. Introductory examples typically involve length-preserving operations on lists, or ordering invariants on sorting.
Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will show how advanced type systems allow us to express such interactions precisely, and how they support verification of stateful systems as a result.
The talk will include several examples, leading to a verified implementation of a word game (Hangman). I will show how Type-driven Development allows programmers to specify the game rules in a direct and concise style, and how it leads to an implementation, guaranteed to correctly follow the rules by typechecking.

[@chrismueller6974]

This is my first time to see first-class types in action.
Mind blowing!

[@schneider.felipe]

One of the best talks I've ever seen! And it has aged so well! A lot of the concepts went on to live in many today's programming languages!

[@miscibi]

rightNow : Me -> Edwin TDD (S Haskell) -> Mind Blown
Thank you Edwin for the clear, mind blowing and funny talk!
And thank you Scala World for the great format! Also, make more bets guys!!!

[@pezo1919]

Thats so cool! I hope JetBrains will adapt it :)

[@MrBaudin]

Amazing talk, thank you!

[@idemchenko-js]

Impressive!

[@-AsL-]

Beast!

[@Kirfx]

insane )))

[@wliaputs]

The automatic code completion part is mind blowing, never thought it could be automated, what’s the model or theory behind this?

[@GildedHonour]

50% of the time:
so, so, so, so, so, so, so, so, so, so,
oh, by the way ... so, so, so, so, so, so,
right .... so, so, so, so, so, so, so, so, ...
so, so, so, so, sooooooo
so, so, so, so, so!

[@jwj410]

and the other 50% was incredible content. Public speaking without pauses aint so (so so sooo so) easy

[@SimGunther]

So so so so so
so so
soso so so so so so so so so
Um so um um so....
See how annoying it is for people to nit pick something that has nothing to do with the excellent content?