Galois’ formal methods division has published some interesting research. “Coverset Induction with Partiality and Subsorts” helps establish how to prove mathematical statements about a more computationally realistic set of recursive functions than standard methods have traditionally allowed. It’s a small step forward for formal provability, but it’s still more roughly in the space of designing helpful tools for FAI design than most people out there are making.
And maybe we can just sub-contract them to build an FAI all on their own? As their website says, “Galois’ mission is to create trustworthiness in critical systems. We’re in the business of taking blue-sky ideas and turning them into real-world technology solutions.”
I’m just imagining the phone call now, “So… I’ve got this really, really blue-sky project for you.”
See on corp.galois.com
