For what it's worth I'm now working on a proof assistant so yeah, that's the game plan. I think the straight line case for the solver is probably OK but there's a huge range of optimisations out there and it's far too easy to introduce errors there.