Lambda the Ultimate

Am I dreaming to hope that more verification is a good thing, and is on the way?

CakeML: a project that aims to make proof assistants into trustworthy and practical program development platforms. At the heart of our approach is a new dialect of ML, which we call CakeML. CakeML is designed to be both easy to program in and easy to reason about formally in proof assistants for higher-order logic.

I'm not saying nobody else is doing / has done cool verified stuff (e.g. cf. verified PreScheme, et. al.), I am just posting this because I'm excited that this project is apparently alive and kicking. I just want to be able to "sudo apt-get install" some day and start programming away, feeling like there's a little bit more safety-blanket feeling there.