New Logic for Programmers (and the future of this newsletter)

<p>So first the immediate news: I just released version 0.14 of <a href="https://logicforprogrammers.com" target="_blank">Logic for Programmers</a>! This release is pretty similar to 0.13. There are a few rewrites but the vast majority of the changes are layout, copyediting, and technical editing. Full notes <a href="https://github.com/logicforprogrammers/book-assets/blob/master/CHANGELOG.md" target="_blank">here</a>. </p> <p>In related news, I've started doing test prints of the book:</p> <p><img alt="Two test prints of Logic for Programmers" class="newsletter-image" src="https://assets.buttondown.email/images/958bdc79-fa06-4bce-b0a8-6e5ecfe8f2e0.png?w=960&amp;fit=max" /></p> <p>There's not a whole lot left to be done. I've gotta fix up some diagrams, do more formatting and proofreading, incorporate some fixes raised by readers, and make a website and back cover. After that, the book should be ready for 1.0. I'm aiming to have print copies purchasable by the end of June!</p> <hr /> <p class="empty-line" style="height:16px; margin:0px !important;"></p> <p>Now the big news: starting August, I'll be a full-time employee of <a href="https://antithesis.com/" target="_blank">Antithesis</a>, a generative testing platform. Officially my role is "developer educator", and I'll be tasked with making "property-based testing, fuzzing, fault injection, <a href="https://hegel.dev/" target="_blank">Hegel</a>, <a href="https://github.com/antithesishq/bombadil" target="_blank">Bombadil</a>, and the Antithesis platform understandable to everyday engineers". So the same kind of work I do now, except with far more support and a matching 401(k). </p> <p>I already have three pages of topic ideas you have no idea how excited I am about this </p> <p>So how is this going to affect the newsletter? First, I want to make clear that this is <em>not</em> going to become an Antithesis newsletter. My Antithesis-related work is going to be on their official platforms. I do think one of the best ways to make a topic "understandable" is to write foundational material that's useful to all engineers, whether they're invested in the topic or not. I might share links to things I make along those lines, but they'll be just that, links.</p> <p>At the same time, the content of <em>this</em> newsletter will change a little. Property testing and fuzzing aren't the same as formal methods, but a lot of the foundations overlap, especially in how we think about properties and correctness. I don't know for sure yet, but I suspect that I'll start biasing this newsletter away from Antithesis related topics. So there will probably be less theoretic things like <a href="https://buttondown.com/hillelwayne/archive/what-does-undecidable-mean-anyway/" target="_blank">what does undecidable mean</a> and <a href="https://buttondown.com/hillelwayne/archive/some-tests-are-stronger-than-others/" target="_blank">Some tests are stronger than others</a> and more history and software weirdness things like <a href="https://buttondown.com/hillelwayne/archive/why-do-we-call-it-boilerplate-code/" target="_blank">Why do we call it "boilerplate code"</a> and <a href="https://buttondown.com/hillelwayne/archive/finding-hard-24-puzzles-with-planner-programming/" target="_blank">esoteric programming paradigms</a>. </p> <p>The other change is going to be frequency. For the past six years I've kept updates to (mostly) a weekly schedule. For the past six years I've also been totally self-employed. I don't know how much time I'll have with a full time job! Once I'm settled in I'd like to keep writing newsletters, but it might slow down from weekly to biweekly or monthly. We'll feel it out as we go. </p> <hr /> <p>Anyway, this has been a pretty software-light newsletter, so let's close out with a fun thing. <code>f(x) = x+2</code> is a <strong>monotonically increasing function</strong>: increasing <code>x</code> increases <code>f(x)</code> and decreasing <code>f(x)</code> decreases <code>f(x)</code>. Similarly, <code>f(x) = -x+1</code> is monotonically decreasing, and <code>f(x) = x^2</code> is neither.</p> <p>While working on the book I realized that the <code>all</code> quantifier is monotonically false with respect to adding elements and true with respect to removing them. Let <code>A(set) = all x in set: P(x)</code>. Then if <code>A(S)</code> is false, <code>A(S | {e})</code> is also false, and if <code>A(S)</code> is true, <code>A(S - {e})</code> is also true. <code>some</code> goes the other way: if it's true, it's true if you add an element, and if it's false it's still false if you take one away.</p> <p>An interesting consequence is that <code>all</code> <em>must</em> be true for the empty set, because if it was false it would be false for all values! This is another justification why, in Python, <a href="https://buttondown.com/hillelwayne/archive/why-all-is-true-prod-is-1-etc/" target="_blank"><code>all([]) == True</code></a>.</p> <p>Similarly, in temporal logic: <code>always A</code> is monotonically false with respect to system behavior and <code>eventually A</code> is monotonically true. I realized this when messing with this <a href="https://quickstrom.github.io/ltl-visualizer/" target="_blank">LTL visualizer</a> my friend (and soon to be coworker!) Oskar Wickström. I think this is pretty neat!</p> <p class="empty-line" style="height:16px; margin:0px !important;"></p>