Hacker News Reader

Has there been a formal specification/model that we can check? I love circular buffers but I'm curious how we know that the design is correct with respect to the stated properties.

I did a bit of link diving to the various blog posts and sites but haven't been able to find it. Would be nice, if it exists, to have it front and centre.

View on HN

As far as I know, it hasn't been formally verified.

Andrea Lattuada (https://andrea.lattuada.me/) is more likely to have done work in his implementation of the algorithm than I did on mine.

I have run the testing with various dynamic analysis tools, but for sure this isn't formal verification. If someone is interested in doing it, happy to chat with them!

Shouldn't be that hard to at least model check it in TLA+ I would have thought (albeit potentially more complex if trying to account for weak memory).

Reply on news.ycombinator.com