> The resolution (decompression) of such backreferences in an imperative context is trivial, but uses lots of invariants that make it hard to prove correct. In a purely functional context, it is non-trivial to find data structures that are fast enough. We decided to stick with purely functional algorithms, as they can be verified directly using Coq, and optimization of purely functional programs is interesting for its own sake. In our current verified implementation, this is the slowest part. The benchmarks in Appendix 0.A support this claim. We already have figured out an algorithm with better performance, but we are not yet done proving it formally correct; we will not get deeper into this algorithm in this paper.
There are many ways verify programs; the authors of your linked paper just chose a method that resulted in a slow binary. Alternatively, one can build a model of an imperative language (C) and prove that an imperative programs meets some specification.
I think it's absolutely viable and arguably should become the standard approach in time
I think it's overwhelmingly due to very very few people developing new greenfield software who are comfortable working with formal models
The talent pool for ATP devs is very small and specialized and they've only been financially justifiable when working on an established mission-critical system, like Lean's creator working at MSFT to catch Windows 7 bugs with SMT solving
Ironically I think these cases where formal models are clumsiest: using FP langs to retroactively model to C/C++ legacy programs
The benefits of formal verification are 10x easier to achieve if they are the foundation vs shoehorned in after IMO