Carl Kadie

Stream: new members

[Carl Kadie]

Greetings, I'm Carl -- an open source developer in the Seattle area. I'd love to learn how to use Lean for simple proofs of algorithm correctness. I see that Northeastern University did just this in their CS 2800 class, but only their syllabus is online. If anyone can suggest links to videos, papers, books, etc., about algorithms and Lean, I'd much appreciate it.

[Chris Bailey]

"Logical verification" is not strictly focused on algorithms and uses Lean 3, but I think it's really good. There's a PDF/book, a repo with the accompanying code, and videos for the lectures: https://lean-forward.github.io/logical-verification/2021/

The software foundations series has a book (volume 3) on algorithms. It's in Coq, but the systems have similar foundations. https://softwarefoundations.cis.upenn.edu/

Mathlib4 is still sort of a fledgling, but there's some early CS stuff in there (heapsort, union find). The implementation of RBMap in the prelude is also pretty interesting. Lean has pretty good editor support, so reading source code and using type hints/go to def stuff is actually pretty productive.

[Chris Bailey]

Actually the "Other Courses" section of the lecture notes you linked has a lot of good sources. Both of the things I mentioned are in there.

[Carl Kadie]

Thanks for the verification links. I especially liked this Insertion Sort correctness proof (via Coq). I also found a Lean-verified proof for Insertion Sort's stability.

I'm personally most interested in probability-related algorithms. For example, I love the algorithm below for returning a uniform-random line from a text file in one pass. I'd love to eventually create a verified proof that the returned line is chosen uniformly.

Until then, I'll keep by eyes open for more progress in verified program correctness.

-- Carl

# Return a random line from a text file.
# Select the line uniformly.
# If the file is empty, return None.
# Make only one pass through the file.
# Use memory proportional to the longest line.

import numpy as np

def random_line(file_name: str, seed:int=0) -> str:
    rng = np.random.RandomState(seed)
    with open(file_name) as f:
        random_line : str = None
        for index, line in enumerate(f):
            if rng.uniform() < 1.0 / (index + 1):
                random_line = line
        return random_line