Add blog post for my final project

[InnovativeInventor]

Closes #510.

[sampsyo]

Nice work here, @InnovativeInventor! This was a clear explanation of the approach and the goal, and the outcome seems more or less expected. You'll see one big question in my inline comments: did you find any bugs? 😃 Either way, it might be nice to state that outcome in the post somewhere.

[sampsyo]

Hi, @InnovativeInventor! Looks like you've added a few commits here—let me know when you think this is ready and I'll take another look (and publish).

[sampsyo]

Just one last reminder about the above, @InnovativeInventor—let me know when it's time to take another look.

[InnovativeInventor]

I've been thinking about better ways to explain this idea (the old version of the blog post was quite dissatisfying and seemed jumbled).

To make it easier to understand, I added a new section titled:

+ ## Interlude: Abstract Interpretation
... [parts of diff removed] ...
+ The key idea we will exploit in this blog post is that there are many different
+ semantics (ingredient no. 4) for which the *same* concrete domain (1), abstract
+ domain (2), programming language syntax (3), and abstract transformer (5) are
+ still sound for!

Hopefully it helps!

---

For some context: this idea came out of a side project of mine (with Ben Kushigian and a few others at UW) where we're interested in test completeness: doing (provably sound) program verification via testing. A test suite is complete iff passing the test suite implies the spec is satisfied; equivalently, a test suite is complete if adding another test won't catch more defective implementations. Investigating complete test suites is interesting for a few reasons, but one thing that it addresses is "what is a good spec?" -- if you like every example in a compete test suite, you are committed to liking the spec (or a refinement of it).

More relevantly to this blog post, there is an notion we're developing that is dual to test completeness -- a complete implementation. An implementation is complete if it can (possibly non-deterministically) witness all the valid traces that are allowed under the spec. My initial idea was to do a "complete implementation" of the standard (1 + $\epsilon$) model of floating point error. But this is not necessary: one can quite easily cut down on the search space, which is the approach I ended up going with.

[sampsyo]

Nice! This seems great. It seems like this version gets across that underlying motivation a bit more directly. Nice work!