I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a diffic

I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'. I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'. Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C. Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.