Last week on a live stream, I introduced structural verification and applied it to an example data model from my work. Here is where you can find that recording, plus an explanation of what Alloy is and why we might use it.
Today, I’d like to share a recording with you from the follow-up stream. I paired with Alloy board member and all-around structural verification expert Hillel Wayne to improve the Alloy that I wrote.
For the first several minutes we’re trying to get the live stream to work (whoops), but once we figure it out, we get into some interesting stuff. I have deliberately auto-advanced this link past the first ten minutes. Believe me, you don’t want to see that ;).
|
As per the description:
This recording serves as a standalone introduction to structural verification with Alloy on a particular problem that work on—pipelines for transforming NASA LandSat satellite data.
Watch to see:1. An introduction to the data model
2. An introduction to the boundaries that need to be implemented
3. A tour of the way I expressed those boundaries in Alloy
4. (The fun part) Hillel Wayne and I pair to make this expression of the data model more concise and more useful.
Among the concepts covered:
– A lot of basic Alloy syntax
– Predicates as expressions of system boundaries
– Using checks to prove properties of the data model
– Adjusting the way the data models get represented in the diagrams
With bonuses, including:
– Hillel talks about some of the history of the Alloy syntax
– Sat solvers: which one to use, and tradeoffs between them
– Russian balancing balls!
I hope you enjoy it!
If you liked this piece, you might also like:
How to Jump-Start a New Programming Language, or maybe, even, gain a more concrete mental model of the one you already use!
Lessons from Space: Edge-Free Programming, which also explores an Android app’s design and the engineering choices behind it (plus, cool pictures of rockets!)
How does git detect renames?—This piece is about how git detects renames, but it’s also about how to approach questions and novel problems in programming in general