Understanding liquid types, contracts and formal verification with Ada/SPARK

There are programming concepts that are not widely known. Most of the time this is due to languages not implementing such concepts or the way they are taught and presented make them seem a lot more technical and not-so-practical. In this talk, I would like to explain what liquid types, contracts and proving code are. The examples will use the Ada programming language as it supports all of these features out of the box and it is a very easy to read and understand language. The examples given will also try to show the practicality of these features, as they are a set of wonderful techniques that tend to be overlooked in "real world" programs.