I've just now watched the talk [1], thank you for the link, but I feel his conclusion actually backs up my position: "Pure, strict functional programming is a very short path from a program to a correctness proof". Admittedly, the tooling in this area has yet to arrive. But for a bespoke contracts language, I wouldn't be put off by that.
Well, I'd be very surprised if Leroy had said anything else. FP is his field, after all. But this view is far from the consensus in the software verification community. Bear in mind, though, that both (somewhat intersecting) disciplines of PL (especially FP) and formal methods have a lot to answer for. Both have made a lot of grand promises over the past 30 years, and both have failed to deliver anything near what they'd promised.
