search

bbchallenge / bbchallenge-proofs

Mathematical proofs of the bbchallenge project.
Creative Commons Attribution 4.0 International
16 stars 6 forks source link

RFC: a more rigorous proof style for algorithm correctness #8

Closed meithecatte closed 1 year ago

meithecatte commented 1 year ago

Currently, the proof for the cyclers decider pretty much only restates the theorem statement, begging the question. I'd like to suggest a more rigorous style for proving these kinds of statements, directly inspired by how one would go about convincing a computer of the correctness of an imperative program. Namely, we state loop invariants, and then prove that they hold by implicit induction on the number of loop iterations.

This PR demonstrates how this approach would work for the cyclers decider. If there's interest in adopting this, I'd be willing to work on analogous proofs for the other deciders.

meithecatte commented 1 year ago

In the Discord, there is consensus that we should instead be going in the opposite direction, leaning on the Coq proofs when necessary. In hindsight, I agree.