E2E: Erik Meijer and Leslie Lamport - Mathematical Reasoning and Distributed Systems

Posted By: Charles | Mar 9th @ 12:06 PM | 34,846 Views | 11 Comments

A distributed system is one in which the failure of a computer you didn't even know existed can render your own computer unusable. -Leslie Lamport.


Leslie Lamport is a computer scientist and mathematician best known for his work with distributed systems. In fact, Dr. Lamport’s research contributions laid the foundations for the theory of distributed systems. He currently works in Microsoft Research where most of his time is spent developing formal semantics (with mathematical logic) for specifying and reasoning about algorithms.

Here, Dr. Erik Meijer, computer scientist and programming language/library designer, sits down with Dr. Lamport to discuss several aspects of Dr. Lamport's body of work in computer science.

Dr. Lamport's TLA, the Temporal Logic of Actions, is a logic for specifying and reasoning about concurrent and reactive systems. TLA+ is the latest incarnation of this formal specification toolset.
Rating:
10
0
#Mar 9th @ 3:05 PM
ShinNoNoir
ShinNoNoir

"When you understand something, then you can find the math to express that understanding. The math doesn't provide the understanding."

 

 That's just one awesome quote Smiley

#Mar 9th @ 3:09 PM
Charles
Charles
Welcome Change

Agreed. Leslie is full of wisdom. It was a pleasure to meet him.
C

#Mar 9th @ 3:23 PM
Richard.Hein
Richard.Hein
Stay on Target

@Charles:  So, maybe PEP is related to concurrency after all. (re: http://channel9.msdn.com/forums/Coffeehouse/534390-Friday-Non-Sequitur-Why-we-dont-implode/)

#Mar 10th @ 10:36 AM
exoteric
exoteric
newspeak :: a -> IO ()

This reminds me of Wesner Moise's article about specification languages.

I'd be interested in hearing more precisely what Microsoft is using TLA+2 for.

 

http://wesnerm.blogs.com/net_undocumented/2009/02/specification-languages.html 

 

...And whether there is a convergence underway with all the specification languages at Microsoft (AsmL being another; Spec# being another still, etc.)

#Mar 10th @ 11:35 AM
Charles
Charles
Welcome Change

Will do. I think we'll dig into TLA specifically next time Leslie is in town.

C

#Mar 10th @ 2:55 PM
Charles
Charles
Welcome Change

Another great quote is at 48:48 (excellent time point, too): “The mathematics of computing; things like sets and functions and logic, are to computing what real numbers are to physics.”

 

C

#Mar 10th @ 4:15 PM
Bass
Bass
A computer once beat me at chess, but it was no match for me at kick boxing.

He is also the author of LaTeX. Smiley

#Mar 10th @ 4:24 PM
Charles
Charles
Welcome Change

He is indeed. He and Erik didn't talk about that, however. The conversation was squarely focused on mathematical reasoning, algorithms and distributed systems...

C

#Mar 10th @ 8:55 PM
N2Cheval
N2Cheval
Why not null?

That was very interesting and gives pause of thought on my software designs.

 

Thanks for the interview.

Microsoft Communities