Project updates, request for help, braindump
Update on Major Projects
I've finally, finally started drafting out the crossover project. And only two months late! Right now the outline is almost a thousand words. This is gonna be a monster.
For those of you just joining us, I interviewed 18 people who used to be traditional engineers and are now software engineers. I'm doing this to get a better sense of what makes software different. Answer? Not much.
Draft 2 of This is How Science Happens is about 80% done.
"Introduction to Alloy" is falling by the wayside because I want to devote more resources to tlacli.
Speaking of tlacli...
tlacli started out as a short script for running TLA+ model checking from the command line. It's not as powerful as the Toolbox, but it's aiming to be more convenient. You don't need a full IDE, you don't need to configure all the parameters, you don't need to create new projects for each spec. Just do python tlacli.py and you're checking a model.
People do not use inconvenient tools, regardless of how powerful they are. I call this the "flossing principle": only 30% of Americans floss daily. It takes like 2 minutes! If people aren't going to spend two minutes flossing, they're not going to use annoying tools.
This isn't an indictment of people. It's accepting that UI is really, REALLY important in tool adoption. Which is why I'm improving tlacli. As it gets more sophisticated, though, it makes more and more sense to make it a proper pypi package. Then people don't need to clone it or mess with file paths, they can just do pip install tlacli and then tlacli check ....
If anybody's interested in helping me turn this into a package, I'd love some advice or contributions! Packaging looks like one of those things that takes a beginner a day to learn but someone who's experienced like 20 minutes, hence me asking y'all for help :). I opened an issue here so you can post there if you want to help. Otherwise we might get six people doing it simultaneously, which is going to waste at least five peoples time.
Random Thoughts
I feel bad ending on a request for help, so here are some ideas that have been bouncing around in my head:
Software Cognates
In Elixir you write functions like split/2, where the /2 means it takes two arguments. It does this because Erlang does this. Erlang does this because Prolog does this. I have no idea where Prolog got this.
This makes /2 a cognate: a language feature that persists through descendant languages. Similar cognates: BCPL's =-as-assignment, Smalltalk's inject, wherever $var comes from. Cognates are important because it lets us figure out how languages evolve, and how different languages are related. Probably a lot of interesting stuff you can do here, should talk to actual linguists about this.
Smart Groups
Define a group as a stateful collection of specified elements (like users). Define a static group as a group with explicit "add/remove" operations: there is a direct relation between an object and the group. A smart group, then, is a group where membership is determined by a predicate. Such as "all users created after $DATE". Smart groups are a really popular feature but add a lot of complexity. In theory you can use arbitrary predicates, but in practice basic sanity rules out plenty of predicates. The predicate must be a pure function, otherwise membership is not stable across checks.
A more interesting restriction: predicates have to be "first-order" and cannot include "group membership" as a possible subpredicate. Otherwise you can get x ∈ A if x ∈ B and x ∈ B iff NOT (x ∈ A). Those are mutually contradictory and your smart groups are inconsistent. So don't allow smart group predicates to include other groups.
(I think this also goes away if you get rid of NOT. Why does NOT make things so complicated? See also: Datalog's lack of negative literals, Petri net inhibitor arcs. There's something deeper here- probably a connection to Turing completeness or something)
Other interesting question about smart groups: resource constraints. Depending on your expressivity you might have to recalculate smartgroup membership every time anything in the system changes, which is crazy expensive. How do people actually do it?
Self-Service Checkout
Really crazy state machine! Lots of program invariants, f.ex you can scan liquor and continue checkout but have to show ID before being able to complete purchase. How do you implement couponing? Consider sets {A, B} and {D, C}, both with a "buy one get one free" coupon. Coupon activates for bag [A:1, B:1], [A: 2], [C:1, D:1], but not for [A: 1, C: 1]. So some notion of "equivalent items" for each coupon. Probably hell of a data model.
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.