Last month I announced my new book, Logic for Programmers, is now available in print. It's long overdue to talk about what this book actually is and why I think most software engineers would find it worth reading. There are two fields of math indispensable to programmers. The first, arithmetic, concerns manipulating numbers. Everybody learns this in grade school. The second, logic, concerns manipulating boolean expressions. A few lucky programmers learn this in college math classes, and everybody else picks it up through osmosis. So the book starts with a crash course in logic, maybe 16 pages of basic math. Then, because this is logic for programmers and not for academics, the next 200 pages are all applications. How to refactor better, how to test better, how to make better data models, etc. So, what do you actually get by learning logic? Three things. First, it opens up a lot of useful software techniques. Once you know some logic you can do things like property-based testing, constraint solving, goal planning, requirements analysis, lots of fun stuff. In particular, formal methods is extremely hot in AI right now, and do to basically anything with FM you need to know logic. Your clanker might be able to clank its way through the implementation details but you need to know the fundamentals to make it implement the right thing. That's why three chapters of the book are on various aspects of formal methods. Second, logic unifies different-seeming ideas in different areas of software. Did you know there's a deep connection between the Liskov Substitution Principle, database migrations, and Hyrum's law? Did you know that the "Rule of Least Power" and "Make Illegal States Unrepresentable" are consequences of the same essential tradeoff? Third, knowing logic just helps you understand stuff better. One database expert said the book had the most lucid explanation he's ever seen of inner and outer joins. But that explanation only works because the book already taught set builder notation and Cartesian products, after which it's pretty easy to formally define joins! So, if you want a deeper understanding of your craft and exposure to lots of cool and useful techniques, I'd strongly recommend learning logic. As for why to learn it from my book? Because it incorporates feedback from fourteen domain experts and fifteen public alphas. I spent three years of my life making this the absolute best book on the subject I could write. You can buy Logic for Programmers as a PDF, epub, or stack of bound paper. Check out the link for more info and a free sample! logicforprogrammers.com/

I think you are vastly vastly overestimating the number of devs familiar with FP, and the number of devs familiar with FP who also know type theory

Multiball mode

I feel the same way when I meet a developer that doesn't know about temporal existential hiding in specification refinements. It's like software development 101

New model announcements should preregister their benchmarks like medical trials do "Timefarble 9.6-smash got 82.9 on SplumpkinBench and Opus 5.5 got 80.3!" I know what all those words are supposed to mean and have learned NOTHING

Man it's good I take weekends off, missed wahtever nonsense this is subtweeting

Ah, yeah, I guess that's not super clear from my description. You can use each any number of times

Time to introduce him to logic mazes en.wikipedia.org/wiki/Logic_…

Are there any languages, aside from the ones that require all functions to be total, where `tail([]) == []`?

Empiricism vs rationalism vibes

What’s most interesting to me is we have hit half a dozen bugs **not** found by LLMs statically reasoning over code. There is alpha yet

I have never heard of C+@ and am extremely curious

The grimly funny realization for me is that the optimal amount of "making a complete fool of myself by trusting an AI" in my life is >0

I really wanna see a corpus of the properties, since that's historically LLMs weak point

Woah! I only know this from Petri net reachability, this is a cool use case!

Dafny has no concurrency, very little IO, and LLMs are terrible at coming up with contracts

Here yah go arxiv.org/pdf/2104.13866

Yeah, the ordering makes it equivalent to Petri net reachabilty

Walk me through how this would work with S=<0,0,0>, G=<9, 9, 9>, D={<0,0,1>, <0, 1, -9>, <1, -9, -9>}?

What if there's no way of ordering the linear combination so that all of the coordinates remain above zero?

You're boring