Thinking for Programmers - Leslie Lamport

Thinking for Programmers | Build 2014 | Channel 9:
"Leslie Lamport inventor of Paxos and developer of LaTeX introduces techniques and tools that help programmers think above the code level to determine what applications and services should do and ensure that they do it. Depending on the task, the appropriate tools can range from simple prose to formal, tool-checked models written in TLA+ or PlusCal (Algorithm Language)"


 Using mathematical models to describe behaviors of programs.

For example, used for inspecting Amazon S3 and XBox 360,
and found real bugs, that could not be detected by testing.

The PlusCal Algorithm Language @ Microsoft Research

P-Syntax

while x > 0 do
  if y > 0 then 
     y := y-1;
     x := x-1
  else 
     x := x-2
  end if
end while;
print y;

C-Syntax

while (x > 0) {
  if (y > 0) { 
    y := y-1;
    x := x-1 
  } else 
    x := x-2 
  };
print y;

F-Syntax :)

while x > 0
  if y > 0
    y := y-1
    x := x-1 
  else 
    x := x-2 
print y