Pawel Szulc - Formal verification applied (with TLA+)

Formal methods (and formal verification) promise something that every programmer dreams about - an ability to deliver software that is proven not to fail. Despite them being heavily researched for the past few decades, they seem not to get enough traction. It might be that people are just simply scared of a little bit of math or it could be that even good techniques take time to surface to the mainstream. This talk is here to change that. To convince and encourage you that (at least) some techniques are easy to use and can potentially save you days or even weeks of later debugging.
Pawel will introduce Leslie Lamport's TLA+ - a formal specification tool with a model checker and proof system. The main objective is to see how formal specification can quickly discover issues deeply hidden in the corner cases of your design. You will gain a powerful tool that you will use in your daily routines. Working with TLA+ will also allow you to think more abstractly about your system. This is not a theoretical talk, this lecture begs you to "please try it at home" - you won't be disappointed.

[@TheRedbeardster]

Excellent and reasonable stand-up, Pawel!

[@donha475]

This is great! Love the passion. If I get the time, I would love to learn this. At least give it a try. It's like meta programming! And in theory would be better than learning yet another programming language...

[@archudzik]

Cool talk, thanks!

[@ggzor]

11:11 Little correction. Dependent type systems are on the upper right part of the diagram (Coq). More "simple" type systems like the ones of C, Java, Haskell are on the lower left part.

[@SaMusz73]

What is the correction ? Isn't this what was said ?

[@donha475]

AND... I wonder if TLA will be used by hackers eventually and so we will have no choice but to learn this to write iron-clad systems...

[@mrmorcs]

It looks like the Hillel Wayne talk referenced is ruclips.net/video/_9B__0S21y8/видео.html (two underscores and a zero)