4 ms·
Happy to see progress on this front, but very disappointed that the Datalog based checker is not used. Declarative formulations of these problems are much easi
by j-pb 3y ago
Happy to see progress on this front, but very disappointed that the Datalog based checker is not used.
Declarative formulations of these problems are much easier to maintain, verify, and spec than a imperative (re)implementation.
- vacuity 3y agoI imagine the biggest issue is performance. I'm sure an as-declarative-as-possible approach would be favored if it didn't sacrifice that.
- j-pb 3y agoThe thing is though that a lot of these problems are NP-Hard, so you're often better of with a general problem solver that knows tricks how to optimise the search for the solution, than something hard-coded where it's impractical to do that kind of dynamic programming.
- vacuity 3y agoOn the other hand, there may be a greater gain in specializing the solver for the problem you're tackling. Besides, they can copy some of the algorithms.