I found the reference to Dijkstra interesting because he was a huge advocate for up-front thinking. The difference between Dijkstra and Waterfall is Dijkstra wanted the programmer to think before working on the feature. The order in which features were developed was at a higher level. Waterfall is about listing all the features beforehand and parceling them out to be implemented or scheduled on a monster Gantt chart.

A formal methods based process can definitely be agile, so long as the planning has a feedback loop that includes iteratively-developed finished products.

It is clear to me that formal methods are avoided because they are difficult. It is very hard (I've tried) to learn to verify programs without formal education in the methods. Yet, we can write software without formal methods and we can make it pretty darn correct without proving it correct.

Formal methods will probably not catch on unless a concerted effort is made by CS baccalaureate programs to teach it from the beginning. I fear that most professors are not proficient enough to teach it. So, it will probably be one of those things that may be a good idea but will be unlikely to ever gain traction.