4 ms·
Maybe one could attempt to use a proof assistant to prove that the algorithm is correct?
by cjfd 2y ago
Maybe one could attempt to use a proof assistant to prove that the algorithm is correct?
- nextaccountic 2y agoOr just prove yourself with pen and paper if the algorithm works, using structural induction and other techniques. Then it's just a matter of whether the code follows the spec
- CJefferson 2y agoAt present we are a long way from proving general constraint solvers are correct, as they are built from some many little algorithms that interact in weird ways. It's an interesting area, and I hope we'll get there in the future.
- JonChesterfield 2y agoFor 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.