4 ms·

Thinking for Programmers (2014) [video]

31 points by rrampage 12y ago

leroy_masochist 12y ago
I watched the first 10 minutes and then skipped around a bit. It's an important topic and the substance is solid, and would be great to read a transcript, but I can't watch this whole thing through -- it's too slow-paced and pedantic. Is it just me or is there an epidemic in these technical talks where the speaker addresses the audience like they're 7th graders circa 1994? I.e., explaining what a computer is, what a program is, etc, in excruciating detail? I totally get the importance of fleshing out concepts from the ground up, going from big to small, etc. But in this case, it seems like his hour-long talk could have been delivered in about 20 minutes with a lot fewer elementary examples.
- TY 12y ago
  You can download slides of the talk to get a good overview of where it's going (it's on the page).
  - leroy_masochist 12y ago
    Thanks for the heads-up! I did, and was a fun read.
- suyash 12y ago
  The talk was not designed for just one person, let's say yourself. It was at Build Conf - where programmer experience range from newbie to super experienced. He did a great job covering the basics, most programmers don't understand the basic mathematics of computer programming.
- jqm 12y ago
  MSDN in the title kind of gives it away...
ahelwer 12y ago
I've personally used TLA+ for a work project, AMA. As a general rule, it's excellent for projects where you have combinatorial explosion in state: the rules for state transitions are quite short, but number of behaviours is enormous. This is common in concurrency and distributed systems. When they're first starting out, lot of people think simple state machines are a good target for TLA+ specification, but this is not so. Generally for state machines the number of states is linear with respect to the number of rules you have, so you're better off using something like P which also generates code for you.
- Jtsummers 12y ago
  Years ago I spent some time trying to learn and use Z Notation (wasn't familiar with TLA+ at the time, though it existed now that I'm reading its history). My major hurdle was that this was spent on my own time as my employers weren't interested in applying formal specification tools to our work (real-time, embedded, safety critical systems, it seemed a natural fit to me, especially because the programs were actually fairly small in the scheme of things). My current employers are similarly averse to spending time on formal specifications, but we're doing embedded, real-time, wireless communication systems and again, it's a fairly natural fit (though what we develop is much larger so full post hoc analysis with this tool would be impractical, if not impossible). How difficult, in your opinion, would it be for someone with a math and CS degree (as educational background) to spin up on TLA+ in their spare time? I reasonably have 1-2 hours a night I can spend on this before I'd be eating into hobbies and social activities. I can think of several small projects that would be useful or will be started in a few weeks/months that I might be able to use as demonstrations of the utility of a system like TLA+ (requiring only an analysis of small portions of the protocol, for instance).
  - ahelwer 12y ago
    It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness. Safety is the easy one, and with knowledge of basic predicate logic and set operations you can have a logic puzzle spec written within hours. Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it. I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook. Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.

31 points by rrampage 12y ago

I watched the first 10 minutes and then skipped around a bit. It's an important topic and the substance is solid, and would be great to read a transcript, but I can't watch this whole thing through -- it's too slow-paced and pedantic. Is it just me or is there an epidemic in these technical talks where the speaker addresses the audience like they're 7th graders circa 1994? I.e., explaining what a computer is, what a program is, etc, in excruciating detail? I totally get the importance of fleshing out concepts from the ground up, going from big to small, etc. But in this case, it seems like his hour-long talk could have been delivered in about 20 minutes with a lot fewer elementary examples.

TY 12y ago
You can download slides of the talk to get a good overview of where it's going (it's on the page).
- leroy_masochist 12y ago
  Thanks for the heads-up! I did, and was a fun read.
suyash 12y ago
The talk was not designed for just one person, let's say yourself. It was at Build Conf - where programmer experience range from newbie to super experienced. He did a great job covering the basics, most programmers don't understand the basic mathematics of computer programming.
jqm 12y ago
MSDN in the title kind of gives it away...

ahelwer 12y ago

I've personally used TLA+ for a work project, AMA. As a general rule, it's excellent for projects where you have combinatorial explosion in state: the rules for state transitions are quite short, but number of behaviours is enormous. This is common in concurrency and distributed systems. When they're first starting out, lot of people think simple state machines are a good target for TLA+ specification, but this is not so. Generally for state machines the number of states is linear with respect to the number of rules you have, so you're better off using something like P which also generates code for you.

Jtsummers 12y ago
Years ago I spent some time trying to learn and use Z Notation (wasn't familiar with TLA+ at the time, though it existed now that I'm reading its history). My major hurdle was that this was spent on my own time as my employers weren't interested in applying formal specification tools to our work (real-time, embedded, safety critical systems, it seemed a natural fit to me, especially because the programs were actually fairly small in the scheme of things). My current employers are similarly averse to spending time on formal specifications, but we're doing embedded, real-time, wireless communication systems and again, it's a fairly natural fit (though what we develop is much larger so full post hoc analysis with this tool would be impractical, if not impossible). How difficult, in your opinion, would it be for someone with a math and CS degree (as educational background) to spin up on TLA+ in their spare time? I reasonably have 1-2 hours a night I can spend on this before I'd be eating into hobbies and social activities. I can think of several small projects that would be useful or will be started in a few weeks/months that I might be able to use as demonstrations of the utility of a system like TLA+ (requiring only an analysis of small portions of the protocol, for instance).
- ahelwer 12y ago
  It would not be very difficult to get a working understanding of TLA+. You can separate the language into two parts - specifying safety, and specifying liveness. Safety is the easy one, and with knowledge of basic predicate logic and set operations you can have a logic puzzle spec written within hours. Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it. I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook. Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.