Hi, I'm Hillel. This is the newsletter version of my website. I post all website updates here. I also post weekly content just for the newsletter, on topics like Formal Methods Software History and Culture Fringetech and exotic tooling The philosophy and theory of software engineering You can see the archive of all public essays here.| buttondown.com
Linguistics is about human languages, not programming ones| buttondown.com
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 shar...| Computer Things
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...| Computer Things
History, updates, metrics, and next steps.| buttondown.com
I realize that for all I've talked about Logic for Programmers in this newsletter, I never once explained basic logical quantifiers. They're both simple and incredibly useful, so let's do that this week! Sets and quantifiers A set is a collection of unordered, unique elements. {1, 2, 3, …} is a set, as are "every programming language", "every programming language's Wikipedia page", and "every function ever defined in any programming language's standard library". You can put whatever you wan...| Computer Things
TDD Gone Wrong (Gone Z3xual)| buttondown.com
For sure easier than solving it in SAT!| buttondown.com
There has never been a better time to learn formal specification.| buttondown.com
An explainer for people who don't know computer science and are mildly curious| buttondown.com
Clever code is a bad idea 95% of the time, this is the other 5%| buttondown.com
Short one this time because I have a lot going on this week. In computation complexity, NP is the class of all decision problems (yes/no) where a potential proof (or "witness") for "yes" can be verified in polynomial time. For example, "does this set of numbers have a subset that sums to zero" is in NP. If the answer is "yes", you can prove it by presenting a set of numbers. We would then verify the witness by 1) checking that all the numbers are present in the set (~linear time) and 2) addin...| Computer Things
Requirements, phase changes, and formal methods.| buttondown.com
My April Cools is out! Gaming Games for Non-Gamers is a 3,000 word essay on video games worth playing if you've never enjoyed a video game before. Patreon...| buttondown.com
I have a lot in the works for the this month's Logic for Programmers release. Among other things, I'm completely rewriting the chapter on Logic Programming...| buttondown.com
Logic for Programmers v0.8 now out! The new release has minor changes: new formatting for notes and a better introduction to predicates. I would have rolled it all into v0.9 next month but I like the monthly cadence. Get it here! Betteridge's Law of Software Engineering Specialness In There is No Automatic Reset in Engineering, Tim Ottinger asks: Do the other people have to live with January 2013 for the rest of their lives? Or is it only engineering that has to deal with every dirty hack sin...| Computer Things
Or: why test-first development is not the same as test-driven development| buttondown.com
I know I said we'd be back to normal newsletters this week and in fact had 80% of one already written. Then I unearthed something that was better left...| buttondown.com
Or four kinds, or six kinds, I'm not picky about how you count them| buttondown.com
I occasionally receive emails asking me to look at the writer's new language/library/tool. Sometimes it's in an area I know well, like formal methods. Other times, I'm a complete stranger to the field. Regardless, I'm generally happy to check it out. When starting out, this is the biggest question I'm looking to answer: What does this technology make easy that's normally hard? What justifies me learning and migrating to a new thing as opposed to fighting through my problems with the tools I a...| Computer Things
First of all, I just released version 0.6 of Logic for Programmers! You can get it here. Release notes in the footnote.1 I've been thinking about my next project after the book's done. One idea is to do a survey of new formal specification languages. There's been a lot of new ones in the past few years (P, Quint, etc), plus some old ones I haven't critically examined (SPIN, mcrl2). I'm thinking of a brief overview of each, what's interesting about it, and some examples of the corresponding mo...| Computer Things
Happy new year everyone! I released the first Logic for Programmers alpha six months ago. There's since been four new versions since then, with the November release putting us in beta. Between work and holidays I didn't make much progress in December, but there will be a 0.6 release in the next week or two. People have asked me if the book will ever be available in print, and my answer to that is "when it's done". To keep "when it's done" from being "never", I'm committing myself to have the ...| Computer Things
Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic for Programmers is on sale until the end of Chanukah! That's Jan 2nd if you're not Jewish. Get it for 40% off here. Stroustrup's Rule I first encountered Stroustrup's Rule on this defunct webpage: One of my favorite insights about syntax design appeared in a retrospective on C++1 by Bjarne Stroustrup: For new features, people insist on LOUD explicit syntax. For established features, people want...| Computer Things
I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me thinking about them again.1 We're using TLA+ to model a system that starts in state A, and under certain complicated conditions P, transitions to state B. They also had a flag f that, when set, used a different complicated condition Q to check the transitions. As a quick decision table (from state A): fPQstate' FF-A FT-B TFFA TFTB TTFimpossible TTTB The interesting bit is the second-to-last ro...| Computer Things
Building an intuition for the mathematics behind the "TLA" in "TLA+"| buttondown.com
Just an unordered collections of thoughts on this. In programming languages, nondeterminism tends to come from randomness, concurrency, or external forces...| buttondown.com
Why are scalable systems locally-inefficent, and locally-efficient systems unscalable? Plus, new book release!| buttondown.com
"Stronger" tests are better for determining correctness, while "weaker" tests are useful for localizing errors.| buttondown.com
It's too cold to go outside, so let's talk juggling.| buttondown.com
All languages have numbers, booleans, strings, and lists. What else is out there?| buttondown.com
