RSS Bilingual Reader

It's taken four months, but the next release of Logic for Programmers is now available ! v0.13 is over 50,000 words, making it both 20% larger than v0.12 and officially the longest thing I have ever written. 1 Full release notes are here , but I'll talk a bit about the biggest changes. For one, every chapter has been rewritten. Every single one. They span from relatively minor changes to complete chapter rewrites. After some rough git diffing, I think I deleted about 11,000 words? 2 The biggest ...

Imagine we have a SQL database with a user table, and users have a non-nullable is_activated boolean column. Having read That Boolean Should Probably Be Something else , you decide to migrate it to a nullable activated_at column. You can change any of the SQL queries that read/update the user table but not any of the code that uses the results of these queries. Can we make this change in a way that preserves all external properties? Yes. If an update would set is_activated to true, instead set i...

For the next release of Logic for Programmers , I'm finally adding the sections on Answer Set Programming and Constraint Logic Programming that I TODOd back in version 0.9. And this is making me re-experience some of my pain points with Prolog, which I will gripe about now. If you want to know more about why Prolog is cool instead, go here or here or here or here . No standardized strings ISO "strings" are just atoms or lists of single-character atoms (or lists of integer character codes). The v...

Happy New Year! I'm done with the newsletter hiatus and am going to try updating weekly again. To ease into things a bit, I'll try to keep posts a little more off the cuff and casual for a while, at least until Logic for Programmers is done. Speaking of which, v0.13 should be out by the end of this month. So for this newsletter I want to talk about the Liskov Substitution Principle (LSP). Last week I read A SOLID Load of Bull by cryptographer Loupe Vaillant, where he argues the SOLID principles ...

Last newsletter of the year! First some news on Logic for Programmers . Thanks to everyone who donated to the feedchicago charity drive ! In total we raised $2250 for Chicago food banks. Proof here . If you missed buying Logic for Programmers real cheap in the charity drive, you can still get it for $10 off with the holiday code hannukah-presents . This will last from now until the end of the year. After that, I'll be raising the price from $25 to $30. Anyway, to make this more than just some re...

A couple of weeks ago I started a fundraiser for the Greater Chicago Food Depository : get Logic for Programmers 50% off and all the royalties will go to charity. 1 Since then, we've raised a bit over $1600. Y'all are great! The fundraiser is going on until the end of November, so you still have one more week to get the book real cheap. I feel a bit weird about doing two newsletter adverts without raw content, so here's a teaser from a old project I really need to get back to. Notes on structure...

From now until the end of the month, you can get Logic for Programmers at half price with the coupon feedchicago . All royalties from that coupon will go to the Greater Chicago Food Depository . Thank you!

Hi everyone, I've been getting burnt out on writing a weekly software essay. It's gone from taking me an afternoon to write a post to taking two or three days, and that's made it really difficult to get other writing done. That, plus some short-term work and life priorities, means now feels like a good time for a break. So I'm taking off from Computer Things for the rest of the year. There might be some announcements and/or one or two short newsletters in the meantime but I won't be attempting a...

A while back my friend Pablo Meier was reviewing some 2024 videogames and wrote this : I feel like some artists, if they didn't exist, would have the resulting void filled in by someone similar (e.g. if Katy Perry didn't exist, someone like her would have). But others don't have successful imitators or comparisons (thinking Jackie Chan, or Weird Al): they are irreplaceable. He was using it to describe auteurs but I see this as a property of opportunity, in that "replaceable" artists are those wh...

Last week I ran my first 10k. It wasn't a race or anything. I left that evening planning to run a 5k, and then three miles later thought "what if I kept going?" 1 I've been running for just over two years now. My goal was to run a mile, then three, then three at a pace faster than a power-walk. I wish I could say that I then found joy in running, but really I was just mad at myself for being so bad at it. Spite has always been my brightest muse. Looking back, the thing I find most fascinating is...

New Logic for Programmers Release! v0.12 is now available ! This should be the last major content release. The next few months are going to be technical review, copyediting and polishing, with a hopeful 1.0 release in March. Full release notes here . Three ways formally verified code can go wrong in practice I run this small project called Let's Prove Leftpad , where people submit formally verified proofs of the eponymous meme . Recently I read Breaking “provably correct” Leftpad , which argued ...

Last week I said that this week's newsletter would be a brief history of algebraic data types. I was wrong. That history is now a 3500 word blog post . Patreon blog notes here . I'm speaking at P99 Conf ! My talk, "Designing Low-Latency Systems with TLA+", is happening 10/23 at 11:30 central time. It's an online conf and the talk's only 16 minutes, so come check it out!

In my first interview out of college I was asked the change counter problem: Given a set of coin denominations, find the minimum number of coins required to make change for a given number. IE for USA coinage and 37 cents, the minimum number is four (quarter, dime, 2 pennies). I implemented the simple greedy algorithm and immediately fell into the trap of the question: the greedy algorithm only works for "well-behaved" denominations. If the coin values were [10, 9, 1] , then making 37 cents would...

Greetings everyone! You might have noticed that it's September and I don't have the next version of Logic for Programmers ready. As penance, here's ten free copies of the book . So a few months ago I wrote a newsletter about how we use nondeterminism in formal methods. The overarching idea: Nondeterminism is when multiple paths are possible from a starting state. A system preserves a property if it holds on all possible paths. If even one path violates the property, then we have a bug. An intuit...

( Last week's newsletter took too long and I'm way behind on Logic for Programmers revisions so short one this time. 1 ) In classical logic, two operators F/G are duals if F(x) = !G(!x) . Three examples: x || y is the same as !(!x && !y) . <>P ("P is possibly true") is the same as ![]!P ("not P isn't definitely true"). some x in set: P(x) is the same as !(all x in set: !P(x)) . (1) is just a version of De Morgan's Law, which we regularly use to simplify boolean expressions. (2) is ...

This one is a hot mess but it's too late in the week to start over. Oh well! Someone recognized me at last week's Chipy and asked for my opinion on Sapir-Whorf hypothesis in programming languages. I thought this was interesting enough to make a newsletter. First what it is, then why it looks like it applies, and then why it doesn't apply after all. The Sapir-Whorf Hypothesis We dissect nature along lines laid down by our native language. — Whorf To quote from a Linguistics book I've read , the h...

New Logic for Programmers Release! v0.11 is now available ! This is over 20% longer than v0.10, with a new chapter on code proofs, three chapter overhauls, and more! Full release notes here . Software books I wish I could read I'm writing Logic for Programmers because it's a book I wanted to have ten years ago. I had to learn everything in it the hard way, which is why I'm ensuring that everybody else can learn it the easy way. Books occupy a sort of weird niche in software. We're great at shari...

I'm way too discombobulated from getting next month's release of Logic for Programmers ready, so I'm pulling a idea from the slush pile. Basically I wanted to come up with a mental model of arrays as a concept that explained APL-style multidimensional arrays and tables but also why there weren't multitables. So, arrays. In all languages they are basically the same: they map a sequence of numbers (I'll use 1..N ) 1 to homogeneous values (values of a single type). This is in contrast to the other ...

The excellent-but-defunct blog Programming in the 21st Century defines "puzzle languages" as languages were part of the appeal is in figuring out how to express a program idiomatically, like a puzzle. As examples, he lists Haskell, Erlang, and J. All puzzle languages, the author says, have an "escape" out of the puzzle model that is pragmatic but stigmatized. But many mainstream languages have escape hatches, too. Languages have a lot of properties. One of these properties is the language's capa...

I'm a big (neo)vim buff. My config is over 1500 lines and I regularly write new scripts. I recently ported my neovim config to a new laptop. Before then, I was using VSCode to write, and when I switched back I immediately saw a big gain in productivity. People often pooh-pooh vim (and other assistive writing technologies) by saying that writing code isn't the bottleneck in software development. Reading, understanding, and thinking through code is! Now I don't know how true this actually is in pr...