Oct 05, 2016

Here is a paper by the AWS team that describes their approach to formal methods and which you could find 'tangible' : http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

Sep 21, 2016

Found a much better link :)

http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

Jul 12, 2016

> Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.

I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0].

Perhaps it is because there are myths that are still floating around regarding formal methods that still make developers cringe when they hear mention of them [1].

None the less I couldn't find reference to it in the book... did I miss it?

And besides... unit tests, I'm sure you are aware, aren't good enough alone. They can only increase your confidence in an implementation but they prove nothing.

If we want to start calling ourselves engineers I think we better start looking to how the other engineering disciplines operate. I don't think it will be long before an insurance company comes along and finds actuaries capable of monitoring risk in software development projects and liability becomes a necessary concern.

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

[1] http://www.fm4industry.org/index.php/G-HM-2

Jun 03, 2016

> Don't forget all the Adam Chipala stuff in Coq

Has there ever been another non-trivial real-world program written in Coq (or another dependently-typed language for that matter) other than CompCert?

> Didn't know people actually used TLA.

Oh, far more than Coq; possibly more than Isabelle, even. TLA+ was designed for engineers, and evolved along with careful observation of how it is used by them. Coq is mainly used by type theoreticians to explore proving various mathematical theorems using ITT, and by PL people exploring various PL theories. TLA+ is used by engineers for large-scale software[1][2][3].

> I'd still want a it embedded in a hosting type-theory so I can use it both for proofs and macros.

I'm not sure what you mean by macros (I'm not a type-theory person in the least), but what does it matter if it's a type theory or a set theory? Lamport's thesis was that just as virtually all math proofs don't require type theory, neither do program proofs; indeed virtually none of the algorithm proofs in computer science employ type theory at all. TLA+ is a formalization of such proofs.

The main advantage of TLA+ is that it's as powerful as Coq for verifying algorithms (though it is not designed for proving general mathematical theorems), yet it any engineer can master it in weeks, without learning any new (not to speak of rather exotic) math. Also, it is amenable (and indeed supports) to model-checking, which alone is enough to make it practical. Deductive machine-checked proofs (which TLA+ also supports) are just too time consuming, and have ever been used on full programs only a handful of times. Their main use in industry is to tie together model-checked programs[4].

TLA+'s disadvantage is that it's very hard to extract a program from a TLA+ spec. Translations going the other way (from code to TLA+) have been done a number of times (for C and Java) but only in academia AFAIK. But this is unsurprising as Lamport's (and Dijkstra's) thesis is that effective, practical, program verification can only be done at a level higher than program code (unless it's a small program, specifically written in a simplified matter for the sake of verification, and the very large effort is acceptable -- all three conditions that have been met in the few cases where deductive, whole-program verification has ever been used).

[1]: http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

[2]: http://tla2012.loria.fr/contributed/newcombe-slides.pdf

[3]: http://research.microsoft.com/en-us/um/people/lamport/pubs/h...

[4]: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

Jun 01, 2016

> Note: Amazon's TLA+ reports said they model-checkers for finding bugs that didn't show up until 30+ steps in the protocols. An unlikely set of steps that actually was likely in production per logs. Reading such things, I have no hope that code review or unit tests will save my ass or my stack if I try to clean-slate Google or Amazon infrastructure. Not even gonna try haha.

For those unfamiliar with the reference, there was an eye-opening report from Amazon engineers who'd used formal methods to find bugs in the design of S3 and other systems several years ago [0]. I highly recommend reading it and then watching as many of Leslie Lamports talks on TLA+ and system specifications as possible.

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

Mar 14, 2016

Interesting. Here's the paper amazon published: http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

It's only covering a few use cases and doesn't go into too much detail and shows example code but it seems like using TLA+ has been beneficial for them.

Feb 09, 2016

Have you read this Salvatore? http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

> ... The good thing is that distributed systems are, unlike other fields of programming, pretty mathematically exact, or they are not, so a given set of properties can be guaranteed by an algorithm or the algorithm may fail to guarantee them under certain assumptions. In this analysis I’ll analyze ..

Saw no mathematics in your article.