Three gripes I have with many formal methods projects are (a) choose something about useless to prove, (b) reinvent the wheel unnecessarily, and (c) an assurance argument with huge gaps or on a knockoff of the actual problem. I like that this project does the opposite in each area: a useful algorithm implementation whose proof build on other's projects with end-to-end assurance. Wise. I look forward to reading the paper.
So, what to do next. I suggest working on stuff that isn't getting much attention. For security, realistic proofs are lacking of useful protocols and crypto-constructions from requirements to design to implementation. Also, much foundational software builds on libraries implementing ZIP, PNG, reg ex's, and so on. More verification of those has widespread effect. Program transformations, optimizations of CompCert, integration of covert channel analysis into such tools, more static/dynamic checking, assemblers/linkers, and so on could all use more verification work done with the nice qualities I mentioned about this one. So, any readers thinking of a project might consider the above. That said, it would be nice if this could benefit the average person without formal methods abilities, right?
I thought hard on it. Our systems stuff is usually coded in low-level, imperative languages for performance. Our high assurance work often uses functional programming (or functional style) for specs, tools, and so on. Yet, the limitations and TCB's of those in systems space are huge obstacles. Yet, old Scheme/LISP work showed how to turn a limited functional program into an imperative one step by step by fleshing out its state (among other things). We've also seen metaprogramming & MDD techniques allow us to specify something at a high level with low-level, fast code automatically generated for the target.
I think the trick is to combine all of this: subset of functional programming specifies high-level operation of program and low-level operation of target language (esp fast parts); verification of useful primitives (eg stacks, pointer arithmetic) with high-level interfaces macro-style; a coding style + methodology for going from high functional to low imperative; verified transformations for optimization, macro expansion, and code generation. Each of these exist in some form, most verified in some way. What's left is to verify all of them and their integration. Such an integrated approach might dramatically simplify verification of software by letting developers simply describe it in a high-level, functional way with a step-by-step process to deployment. Verification, depending on talent, might range from manual inspection to machine-checked proofs. Yet, doing it this way should be much easier than converting them to formal verification experts.
What do you developers or formal methods people think of this?