Looks nice. Some explanation for those of us not familiar with Go would've been more educational. Could be future posts, I suppose.

Honestly I don't think there's much in here that's Go-specific other than the syntax itself. I've seen basically the same tricks used in C or C++.

Was there any particular part that felt like it needed more explanation?

Great find and writeup.

As an aside, this is the type of a problem that I think model checkers can't help with. You can write perfect and complicated TLA+/Lean/FizzBee models and even if somehow these models can generate code for you from your correct models you can still run into bugs like these due to platform/compiler/language issues. But, thankfully, such bugs are rare.

Yep. Model checking is for checking that your design is sound, basically, not at all the implementation.

For the implementation, you can use certified compilers like CompCert [1], but:

- you still have to show your code is correct

- there are still parts of CompCert that are not certified

[1] https://compcert.org/

Writing is one of the best ways to learn something. Maybe non-experts learn something by writing about it?

Don't think the entire internet is repeating inaccuracies. :) I also believe there are readers that attempt to learn further than a blog. A blog post can inspire you to learn more about a topic, speaking from personal experience.

If there were no blog posts, maybe there would be no HN I believe.

There should be a place for non-experts. One could remain skeptical when they read blog posts without hating blog posts about complex topics written by non-expert.