Hacker News new | past | comments | ask | show | jobs | submit login

Anecdotally, the team I was in in AWS needed to build a complicated component, one that, should it get it wrong, would be disastrous for the service.

They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production.

They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task.

It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear.

Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code.

In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.




Ive read a lot of industrial use of formal methods. If the method is easy, then almost all of them say what you said about the coding phase. I'll add that competing methods have code generators: Abstract, State Machines and B Method. ASM's look a lot like PlusCal with usability for about anything. Asmeta is one of tools with code generator. I think most doing it for B commercially use Atelier B and ProB. ProB does TLA+, too.

Now, far as TLA+-like stuff, tell them to check out SPIN model checker. It's seen more commercial use than most tools. Outperformed TLA+ in one paper but dont know if that extrapolates. Port some of your stuff to it to see what happens.


Lamport claims on his website that Amazon uses TLA+ and has used it for quite a while now. Saying that to confirm plausibility of this story.


Amazon/AWS has published a few white papers about their use of TLA+ and other Formal Methods:http://lamport.azurewebsites.net/tla/formal-methods-amazon.p....

James Hamilton is a fan of TLA+, and talks about its use in Amazon: https://perspectives.mvdirona.com/2014/07/challenges-in-desi...





Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: