Allow Leslie Lamport to explain to you what TLA+ is

Sat down with a good friend who’s in math + economic history.

He’d taken me to school at the gym, introducing the Thai boxing exercise “kick the heavy bag” 45-seconds-per-leg. Brutal. Loud. I can perhaps recommend it. Afterwards at Nobes, enjoying a traditional meal of potatoes, gravy and vegan kålpudding, he asked me whether math is any use to career programmers.

I hemmed, I hawed. Most programmer activity is not about math. Statistics? Algorithms? Graph theory?

And then I tried to explain TLA+. I failed hard at that, so this short note is a link to better material than I was able to mumble up during eating.

TLA+ is:

a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems.

the TLA+ wikipedia article

The wikipedia article is good. Turns out, Lamport did us one better, he put together a full video course:

“This is the first lecture of the TLA+ video course”, a sun-kissed Lamport intones in the first few seconds. Excellent!

Then, he warns the viewer, that they should consume this course together with the multimedia he has created, at his website. TLA+ Course Lecture 1.

He’s right.

Having watched a few of these caring, teaching, and (mildly) funny videos, I’m becoming a fan. Well-made timed multimedia cues are great. Being told when to stop watching, and downloading a paper, or learning something else – it works well.

(The material is darn interesting.)

Resources made by Lamport on TLA+ abound, and I’m not doing you a service by trying recommend anything less than the real video thing. Any other code repository or tooling he’ll tell you about. He’ll tell you about it while dressed in clown clothes and corny outfits.

For the very interested, and text-oriented, there’s also the hyperbook. A series of interlinked PDF resources, which one can peruse to learn about TLA+. I read a bit of that first, and then switched over to the video presentation. Both are good.

Now, I hope this small note has alerted you to the existence of tons of TLA+ material online, and that you enjoy a whiff of that at some point.

The Stones of Venice

My friend J was at a large fika at my house, holding forth about the perennial mystery of Venice. I whispered the only thing I knew about the mystique of that place: some Englishman’s text about it. J winked and nodded, and knew it, of course.  I have not read this work, except as an escape. I’m a cheat, like that.

The Stones of Venice is a three-volume treatise on Venetian art and architecture by English art historian John Ruskin, first published from 1851 to 1853.

Wikipedia

Now, you can read this massive thing, scanned at Archive.org. If, for some reason, you’re hiding behind your laptop somewhere boring, you could shield yourself with this. Sip long sentences, taking in the stretches of prose.

Or, if you’re not in a place with a laptop, perhaps with only a tiny screen at your disposal: fear not. You may be in for something better.

Read the same work in the Victorian Web’s translation/proof-reading effort. Great collaborative HTML project! They’ve put lots of reference notes in the side-bar, explaining things in the text, and taking us the extra mile in understanding this work’s impact.

Well, one day I hope to have a printed copy of this thing.

Until then, here’s some excellent – unrelated electronic music.

Reading The Morning Paper

You may already know, but there’s a person out there on the Internet making a lot of reading for you. They put out this publication (nearly) daily, which is called The Morning Paper. The eponymous “paper” is a computer science paper, and each report is a walk-through of its contents.

Brilliant stuff, and most of it pushes my mind in some direction. Learning and such is a lot about filling the mind with associations. For me.

Things I learned about during the last fortnight: guiding machine learning using assisted labelling techniques that parse natural language; a really fast JSON filter called Sparser; something about memory management & local reasoning in an upcoming OCaml memory management implementation. Tons of stuff, mostly-digested, for your scanning pleasure.

I enjoy scanning this. Some of it makes me dig out explanations and other thing are possible to scan along, for the thrill of it.

Revamping, again

Ha, the blogging. 

WordPress happens much quicker than I can follow it, which is completely wonderful. Quite a few innovations arrived today: a new editing interface, called Gutenberg.

a Malmö.rb logo
for no special reason
other than ease of uploads

The original critical hit table from the ancient roleplaying game Arduin

This is easy. And way more accessible. I might use it, even.

An Amsterdam Sunday

Stendhal syndrome, Stendhal’s syndrome, hyperkulturemia, or Florence syndrome is a psychosomatic disorder that causes rapid heartbeat, dizziness, fainting, confusion and even hallucinations when an individual is exposed to an experience of great personal significance, particularly viewing art.

We did three museums in one day. That’s really pushing it. But we stayed ahead of the above effects. Here’s what we saw:

After this journey into aesthetics, we relocated to a new  had very good pizzas at Mediamatic ETEN. Elderflower lemonade! Someone speaking Danish tended the bar. “Take a look around!” Aquaponics gardening in a greenhouse with colored LEDs. “Oh, all food here’s vegan.”

Next door was the open-to-the-sky bar Hannekes Boom. The sky was golden and the moon was a thin sliver. Patrons were joyous, the barman was cheerful.

Before heading home to the ironing board and the blogging, we couldn’t resist peeping into the KLIMMUUR CENTRAAL-marked warehouse. My friend C had identified the name to be “Climbing Wall Central”. It was a huge building, very, very tall, covered in handholds and climbing lines. In the middle of the room, there was a group of tables where people could enjoy themselves, or eat something. A non-ascetic place! We bought ice-cream and lounged in a huge couch outside in the evening light.

Boats of all types rushed by. Suddenly, it was time to get back. We discovered a shorter path to walk home – a boon.

An Amsterdam Saturday, a sketch

Amsterdam in harsh, punishing sunlight.

A pre-cold is threatening my weekend, reminding me of bodily frailty, as I and my companion trudge through cobbled streets fraught with traffic peril from onrushing bikes, their bike bells a-clanging.

The street scenes in the city center were the ones I’d been told to expect: tourists toting tourist gear, the smell of people smoking not-cigarettes, everywhere, and lots bikes.

We saw: a cat café, which was not a café – more of a feline prison.

At a critical juncture, we taught ourselves to use Amsterdam’s “collective traffic” (public transportation, as a Swedish-speaking person might say it). That was good. Our reach extended, we grasped for better and fancier environs. The plan was to do something more cultural.

Then, a cup of espresso quickly followed by a well-chilled ginger ale, and in we went to the Museum Het Rembrandthuis. We got an etching-and-printing demonstration, as well as a glimpse of an oil-paint-making demonstration.

We then trudged and traveled to get to our hotel. It was good.

Today I also learned about Happy Cow, a search engine for vegetarian eating. Here’s a sample search.

Having used it, we then promptly ditched all those finely annotated search results, threw caution to the wind, and frequented a recommended Indonesian place: Kartika on Overtoom 68. “Sorry, we only have two fixed options: the vegetarian one, and the other one. Serves two, at minimum.” We agreed to the veg option and were inundated with amazing dishes in bowls, on a long metal warmer. Food was enumerated, then enjoyed. Thoroughly.

After this, a stroll in the park, as the last rays painted immaculate contours around everything. A stand-up comedian was entertaining a big audience. People in the park had not yet given up on the park-life and were frolicking on grass, playing instruments and enjoying themselves.

 

 

Ruby feature: Regular Expression replace once

About a year ago, programmer Tony Arcieri posed a question on the Ruby language bug tracker:  Why was Thread.exclusive deprecated?

Among the answers to this question, Shyouhei Urabe’s one of the tersest feature descriptions yet: “we already have such thing, to some extent at least”:

/#{@mutex=Mutex.new}/o
  1. The pair of slashes are Regular Expression delimiters.
  2. A Regular Expression in Ruby allows String interpolation, just like the double-quoted String does. The #{} contains interpolated Ruby code.
  3. The modifier o at the end of the Regular Expression stands for “once”. So, the regex engine would keep track of this replacement, and do it just once.

The Malmo.rb named this expression (//o) the face-palm operator.

Malmö Coders’ Book Club

Quick report on Malmö coders’ book club: This was the initial sitting, and we were 7 people around the table. One academic, two leads, and four software engineers. We spoke English, since we were an international crowd.

At least three physical notebooks full of written notes were out, and the conversation was started based on questions people had during their reading. The conversations were personal, kind, and focused. It brings more perspective, to have people of different backgrounds, of different roles.

This was one of the peer groups I’d been looking for. 5 out of 5 thumbs.

PS: We had been reading Michael Feathers’ Working Effectively With Legacy Code.