Beginner Computer Science Examples

Stream: new members

[Mark Fischer]

I've been working my way through formally verifying a Sudoku solving algorithm. It's fun, but my proofs are starting to get seriously out of control and I'm looking for inspiration with how to structure such an effort. Or perhaps just inspiration to keep struggling onward regardless :P

I've been searching, so far the examples I'm finding are either less than 100 lines or way beyond my current abilities (CompCert, for example).

If anybody is aware of some resources that might help keep me motivated, I'd be grateful! :)

[Joachim Breitner]

How did you implement the solver? Functional style (recursive functions etc.), or imperative style (Id.run do, let mut)?

[Mark Fischer]

I haven't solved anything yet, so I don't have an answer to that question. Currently, I'm interested in proving that specific deductive steps are sound. I imagine I'd like to build out combinators on top, so that you can repeat or mix deductions. I don't think any of that would benefit too much from Monads, but we'll see!

[Joachim Breitner]

I’d stay away from Monads and use plain functional programming if possible if you want to verify the code.

[Mark Fischer]

Makes sense to me! Nothing involved with solving Sudoku is necessarily effectfull

[Mark Fischer]

You can kind of see the setup from this picture of a corner region of a puzzle:
image.png

Here 1 is a given, then (without any further deductions) other cells can be any of the other possible values. Proving that 1 can be removed from the set of options on the other cells is as far as I've gotten. I found it trivial to convince myself, but pretty hard to first state the relationship and then to convince Lean.

I've got to generalize this to row-box-column scanning in general, and then generalize it further to find tuples and show that row scanning is just a tuple of size one. Repeated use of scanning for tuples (naked pairs/triplets/etc) is enough to fully solve many beginner/intermediate Sudoku, so it's not until then that I'll need any recursion beyond map/filter in std.

As these things go, I always figure out a hard way first and eventually come around to an easier way I should have noticed from the start. lol