Re:Azure Cosmos DB, a globally distributed database
by dmix on Wednesday May 10, 2017 @02:25PM
(#14310389)
The effort to formalize the database was apparently led by:
> Leslie Lamport the Turing Award winner whose work underpins many of these concepts (and who also wrote the LaTeX document preparation system) and who joined Microsoft Research in 2001
Quote about TLA+:
> As Shukla noted, though, his idea here was to build a database system that could last decades. To do this, he also brought in Lamport to teach the team TLA+. Lamport has long had a special interest in how developers spec out their applications. TLA+ is essentially a formal language for doing just that. “When we started out in 2010, we wanted to build a system — a lasting system. This was the database of the future for Microsoft,” Shukla told me. “We try to apply as much rigor to our engineering as we possibly can. […] TLA+ has been wonderful in getting that level of rigor in a team of engineers to set the bar high for quality.” TLA+, Lamport noted, allows you to do the high-level design of a system in a completely formal way — and because it’s done formally, it can be checked for correctness, too (and to be fair, AWS and others also use TLA+ to spec out their distributed systems). “I don’t want to give the impression that TLA+ is great and I’m brilliant. It’s great because it’s almost entirely based on mathematics,” Lamport added.
> Leslie Lamport the Turing Award winner whose work underpins many of these concepts (and who also wrote the LaTeX document preparation system) and who joined Microsoft Research in 2001
Quote about TLA+:
> As Shukla noted, though, his idea here was to build a database system that could last decades. To do this, he also brought in Lamport to teach the team TLA+. Lamport has long had a special interest in how developers spec out their applications. TLA+ is essentially a formal language for doing just that. “When we started out in 2010, we wanted to build a system — a lasting system. This was the database of the future for Microsoft,” Shukla told me. “We try to apply as much rigor to our engineering as we possibly can. […] TLA+ has been wonderful in getting that level of rigor in a team of engineers to set the bar high for quality.” TLA+, Lamport noted, allows you to do the high-level design of a system in a completely formal way — and because it’s done formally, it can be checked for correctness, too (and to be fair, AWS and others also use TLA+ to spec out their distributed systems). “I don’t want to give the impression that TLA+ is great and I’m brilliant. It’s great because it’s almost entirely based on mathematics,” Lamport added.