Ada is underrated. It has clumsy syntax that turns people off. But it gets many things right that other languages don't even think about. Look for the online book "Ada Distilled" for an intro.
Added: I looked at the video a little bit and it's not very informative. This is old and has some errors and gaps but it's a quick read that gets to some of the good stuff:
http://cowlark.com/2014-04-27-ada/index.html
I'll try to find something more recent that describes SPARK. SPARK is a verification system integrated with Ada that's maybe comparable to Liquid Haskell. There is effort under way to make something like it for Rust.