Blog on Hillel Wayne

I started writing Logic for Programmers because there weren’t any good resources on logic for, uh, programmers.

I am delighted to announce that my book, Logic for Programmers, is now available!

It’s April Cools!

As part of writing Logic for Programmers I produced a lot of “chaff”, code samples and sections I wrote up and then threw away.

Been quiet around here!

It’s April Cools!

What does this print?

The other day a mechanical engineer introduced me to the Hierarchy of Controls (HoC), an important concept in workplace safety. 1 (source) To protect people from hazards, system designers should seek to use the most effective controls available.

All of my budgeted blogwriting time is going to Logic for Programmers.

A toolbox language is a programming language that’s good at solving problems without requiring third party packages.

Last year a client asked me to solve a problem: they wanted to be able to compose two large TLA+ specs as part of a larger system.

In his book On War, Clausewitz defines friction as the difference between military theory and reality: Thus, then, in strategy everything is very simple, but not on that account very easy.

I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall.

It’s April Cools!

A (directed) graph is a set of nodes, connected by arrows (edges).

Picat is a research language intended to combine logic programming, imperative programming, and constraint solving.

Humans are notoriously bad at coming up with random numbers.

This is just a way of thinking about formal specification that I find really useful.

This is my writeup of all the talks I saw at Strangeloop, written on the train ride back, while the talks were still fresh in my mind.

Short version: If X inherits from Y, then X should pass all of Y’s black box tests.

tl;dr annotated AHK scripts here.

Two universal facts about user documentation: Documentation is really important.

img {border-style: groove; border-width: 1px;} I love Autohotkey so much that it keeps me on Windows.

I haven’t written much about TLA+ on the blog since the new learntla went up.

It’s April Cools!

I originally ran this on my newsletter last year but I like it way too much to let it rot in the archives.

I like how easy it is to configure neovim.

A common assumption I see on the ‘net is that NP-complete problems are impossible to solve.

Complexity is bad.

img {border-style: groove;} Someone recently told me a project isn’t real until you do a retrospective, so I think it’s time to do one for Let’s Prove Leftpad.

This is my writeup of all the talks I saw at Strangeloop, written on the train ride back, while the talks were still fresh in my mind.

img {border-style: groove; border-width: 1px; padding: 5px; } Sounds like I should write a post on safety and liveness!

Mimicry is when software X reimplements at a higher level a core feature of software Y.

One of my favorite little bits of python is __subclasshook__.

tl;dr: online TLA+ manual/advanced techniques/examples here.

To celebrate April Fools, some friends and I made content outside our normal brands.

I’m not letting myself work on software content for the website until I finish both the Alloydocs update and the learntla rewrite.

In my 2021 TLAConf Talk I introduced a technique for encoding abstract data types (ADTs).

Alloy is a powerful formal specification language, but it’s historically been weak at modeling concurrency.

A Sudoku Puzzle is a famous Japanese puzzle.

When teaching formal methods, I often get asked how we can connect the specifications we write to the code we produce.

This was originally a newsletter post I wrote back in December, but I kept coming back to the idea and wanted to make it easier to find.

“Don’t write clever code.”

Recently my friend Lars Hupel and I had a discussion on why formal methods don’t compose well.

A couple years back I gave a talk on researching software history, using “linked list interview questions” as an example topic.

There’s not a whole lot on TLA+ technique out there: all the resources are either introductions or case studies.

This is part three of the crossover project.

This is part two of the crossover project.

This is part one of the Crossover Project.

Last month I researched two historical questions.