Modeling Redux with TLA+
hillelwayne.com
Modeling Redux with TLA+
1–10 of 34 posts
Re: Modeling Redux with TLA+
#2Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don't know about any of this, I invite you to take a look.
Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2].
1. https://en.wikipedia.org/wiki/Leslie_Lamport
2. https://www.distributed-systems.net/index.php/books/distribu...
Re: Modeling Redux with TLA+
#3> TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint.
Very cool.
Re: Modeling Redux with TLA+
#4His main site he mentions at the end is learntla.com. That's a good tutorial for using a subset of it that will get stuff done without trying to read a bunch of books on heavier stuff. He and I both also recommend Alloy for a taste in formal methods or blueprints like fouc said since it's designed for beginners with good guides and tutorials. TLA+/PlusCal with its model-checker is better at modeling order of execution (esp concurrency/distributed) whereas Alloy's is focused on structure of your program. Finally, Design-by-Contract combined with property-based testing or AFL-style testing with properties/contracts as runtime checks is probably combo most applicable to most programming languages and situations. If you know conditionals, you can use DbC in a lots of situations.
https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...
Re: Modeling Redux with TLA+
#5Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: https://youtu.be/_9B__0S21y8
If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk.
Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.
Re: Modeling Redux with TLA+
#6Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: https://youtu.be/_9B__0S21y8 If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.
It was 7 lb (3.18 kg) of sesame brittle.
Indeed, an entertaining and practical talk on TLA+.
Re: Modeling Redux with TLA+
#7Any takers for doing this in lisp? ;)
Re: Modeling Redux with TLA+
#8Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don't know about any of this, I invite you to take a look. Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2]. 1. https://en.wikipedia.org/wiki/Leslie_Lamport 2. https://www.distributed-s…
I don't see the relevance on knowing Leslie Lamport to learn about TLA+ - what is the matter? One thing has nothing to do with the other...
Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?
Re: Modeling Redux with TLA+
#9> TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint. Very cool.
Cool and impossible to apply to real world projects due to budget or deadlines.
Re: Modeling Redux with TLA+
#10Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.