Mathematical Reasoning and Distributed Systems by Erik Meijer and Leslie Lamport

https://www.youtube.com/watch?v=3krXn4NsCNI

by adamnemecek • 10 years ago

208 37 10 years ago

youtube.com

jzelinskie• 10 years ago

Interesting to see a Channel9 video on YouTube.

Erik Meijer's genuine interest in the subjects in his videos make them a pleasure to watch.

js8• 10 years ago

I really like his point(s) about mathematics and programming, as he talks about functional programming, especially at 47:20.

pron10• 10 years ago

Lamport has always been in favor of a rigorous mathematical reasoning about programs, but has always warned against looking for a "new math", the "right kind of math", or a "silver bullet math" (in other talks he calls it "weird computer-science math"), as he believes that ordinary math is all you need. So yeah, Lamport is not a big fan of FP (or any PL theory for that matter). He's been fighting the Robin Milner school of thought, or PL semantics in general since at least the early nineties. He says here that once you deal with all the incidental complexity, you're left with the essential complexity, and that is the hard part, and he's skeptical of the ability of "new math" to help solve the problem.

See: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...

nickpsecurity2• 10 years ago

"He's been fighting the Robin Milner school of thought, or PL semantics in general since at least the early nineties. "

What does that mean for those of us that follow the formal methods at a high-level?

zzzcpan3• 10 years ago

Well, his points about necessary hard math and proving correctness resemble those of many in academia, I can understand your bias. But it is a bias and there isn't even a good argument to support it. Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever. But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research.

KirinDave3• 10 years ago

Proofs never actually cover absolutely every possible case

That's precisely what you need to do in order to have a valid proof. I'm not sure why you'd say this?

mathetic2• 10 years ago

> Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever.

This is ridiculous. If not being able to prove everything doesn't help, we should get rid of type systems altogether. Programmers are so complacent and ignorant to what their compilers provide them out of the box, they forget how many brilliant people, proofs, and countless hours it took to create those features.

> But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research.

Well, no. Just because you don't understand or care to learn how much pain and work it took to get rid of seemingly arbitrary restrictions of type systems doesn't mean that it is not considered CS research. You think Rust's region types that literally prevent you from leaking memory without garbage collection came out of a hackathon? Java's generics are a usability improvement, isn't it? Do you have any idea about who designed that? Don't even get me started on any of the features in pure languages.

And even if you were so blind to reject all of these as improvements, psychology and usability of programming languages is an actual CS research field with its dedicated conferences. Here's a master's course [0] from University of Cambridge Computer Laboratory.

[0] https://www.cl.cam.ac.uk/teaching/1011/R201/

pron10• 10 years ago

If there's anyone who works very hard to make formal methods approachable to practitioners, that would be Leslie Lamport. He often says that he's not interested in methods that are not usable by "ordinary" engineers working on large, real-world systems. Amazon now uses his TLA+ to specify and verify many (most?) of their AWS services, and they've learned it all on their own. It's been so successful that managers encourage programmers to use TLA+. This is now spreading to Oracle, too. You can read about Amazon's experience here: http://glat.info/pdf/formal-methods-amazon-2014-11.pdf

I discovered TLA+ when I needed to design a complex distributed database. I learned it in a couple of weeks, and immediately put it to good use. It quickly uncovered some (big!) mistakes in my original idea, and helped me find a solution. So my motivation to learn and use TLA+ was, like Amazon's, 100% pragmatic and not at all academic.

chadcmulligan2• 10 years ago

That's a very disappointing shirt Erik is wearing

tomonl• 10 years ago

It's just his style, if you look him up on Google Images you'll see he always wears shirts like that.

chadcmulligan2• 10 years ago

thats what I meant - it's not as bright as his usual style

jasode• 10 years ago

Fyi... the original video released in 2010 is at channel9 and that website also has download options for offline viewing:

https://channel9.msdn.com/Shows/Going+Deep/E2E-Erik-Meijer-a...

nickpsecurity2• 10 years ago

It was an interesting article. Neat how one scheme was inspired by a bakery. The concern with the red light happened to me. Its timing was odd where I wasn't sure if I'd make it or not but on a road with a high speed limit. I decided to brake at the last moment. Should've worked but tires were bald. I landed in the middle of the intersection with a police officer to my right. So, the "hypothetical" example of Lamport cost me money in the real world. ;)

However, I reject his notion that computation is basically digital, step-by-step process. There's actually at least two models of computation where one is continuous. I gave a lot of detail in the link below:

https://lobste.rs/c/zyj5e1

senderista2• 10 years ago

Re: Lamport clocks and special relativity: I don't think Lamport makes it sufficiently clear that the SR analogy is just an analogy and is not physically relevant. It is perfectly valid to treat the computers in a datacenter as a single inertial reference frame, with a natural notion of simultaneity. (Geo-distributed clocks can still be synchronized, since the Schwarzschild solution defines spacelike hypersurfaces with constant time coordinate.) Logical clocks (which totally order events consistent with their causal relations) are useful (because synchronization is hard), but not physically necessary (because synchronization is possible).

Mathematical Reasoning and Distributed Systems by Erik Meijer and Leslie Lamport

Related Stories