Modeling Redux with TLA+ • Hacker News Board

Re: Modeling Redux with TLA+

#31

Post by 0xfeba » Tue, Mar 13, 2018, 3:42 PM UTC

RubenSandwich wrote: post #13

raister wrote: post #9

Earlier quoted context omitted.

Cool and impossible to apply to real world projects due to budget or deadlines.

People said the same things about unit and integration tests a decade ago.

My company still says that today. All the while saying we should do them, but not impact our velocity. Yeah, okay.

Re: Modeling Redux with TLA+

#32

Post by Nelkins » Tue, Mar 13, 2018, 5:46 PM UTC

raister wrote: post #9

fouc wrote: post #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.

Cool and impossible to apply to real world projects due to budget or deadlines.

Not that unreasonable, depending on what your use case is. There are some good, very approachable guides out there like this one[0].

[0] https://pron.github.io/posts/tlaplus_part1

Re: Modeling Redux with TLA+

#33

Post by moocowtruck » Wed, Mar 14, 2018, 1:16 AM UTC

fouc wrote: post #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.

just remember blueprints can also be wrong

Re: Modeling Redux with TLA+

#34

Post by hwayne » Wed, Mar 14, 2018, 2:51 AM UTC

moocowtruck wrote: post #33

fouc wrote: post #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.

just remember blueprints can also be wrong

Yeah, it's extremely important to note that any correctness technique - tests, types, contracts, formal methods - only provides _more_ confidence, not _complete_ confidence. We have to think of defense-in-depth.