cs6120
cs6120 copied to clipboard
sampsyo
Add blog post for my final project
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).
Just one last reminder about the above, @InnovativeInventor—let me know when it's time to take another look.
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.
Nice! This seems great. It seems like this version gets across that underlying motivation a bit more directly. Nice work!