Started leaving a brick on the lid which seems to work.

Comments URL: https://news.ycombinator.com/item?id=23366320

Points: 27

# Comments: 5

Comments URL: https://news.ycombinator.com/item?id=22403089

Points: 2

# Comments: 0

My experience is that, using TLA+, or other tools like it, encourages you to think precisely about the problem and at the same time exclude unnecessary details. That alone I find useful in terms of the insights it gives e.g. surfacing interesting invariants, or alternatively, invalidating them. In any case, you use the model-checker (TLC) to test these assumptions quite easily, and then bring these invariants into your code, either in the form of assertions, contracts or perhaps in property-based testing. In any case, I would say the process of writing such a specification yields benefits. Perhaps this can best be summed up by something I think Leslie Lamport once said: "If you're not writing when you're thinking, you only think you're thinking."

I should add that despite claims about TLA+ being particularly well-suited to concurrency problems, my implementation targets have never been 'concurrent' in the 'multi-threaded' sense. Rather, they have been single-threaded event-driven state machines, and I personally find that it excels in this space. However, as you will find, in TLA+, concurrency is just a matter of abstraction...

I have found that, because TLA+ doesn't 'generate code', many colleagues struggle to see the tangible benefit. I personally think that there is a gap between the whiteboard and the editor which tools like TLA+ fill very nicely. It's not a panacea or a magic bullet, and like any tool you must still exercise judgement about when to use it, and how to use it effectively, which includes understanding the limitations of the tooling (TLC cannot check arbitrary specifications).

But if I find myself faced with a potentially tricky algorithm, or indeed want to understand an existing algorithm, I reach for TLA+.

This is a multiplier because it allows them to detect and ignore non-problems and work on problems whose solutions _will_ deliver value.

Comments URL: https://news.ycombinator.com/item?id=22380986

Points: 137

# Comments: 50

Still, fascinating to see work like this on real-world code-bases with established languages. You can also see very similar work in languages like Dafny[3].

[1] https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny

- anytime I have some protocol or state machine whose behaviour isn't obvious, I write a TLA+ spec. - the process of writing it clarifies my understanding and leads to new insights. These insights directly inform the code and the tests. - the model checker makes it very easy to check sophisticated properties of the algorithm.

I don't use it all the time, but it's a tool I'm very happy I invested in.

I'm not a power user, I don't use social media apps, just a few daily texts, a bit of browsing, music and podcasts. I also liked the simplicity of the UI.

Ultimately, I got tired of the crappy inbuilt podcast app and lack of decent alternatives. My wife bought me a second hand apple 5s which arrived yesterday.

I already miss the 'swipey keyboard'.

[Used to work at Microsoft, used TLA+ successfully during product development]

Comments URL: https://news.ycombinator.com/item?id=13022404

Points: 7

# Comments: 0

1. A repl would be useful.

2. Better documentation for the individual tools, allowing other editors and toolchains to hook them more easily.

I would say that I found the TLC model checker extremely valuable, but learning what subset of TLA+ it can actually handle (and structuring your specifications appropriately) takes time.

Not sure about enums - seems like something PlusCal would do (if it doesn't already), but I would leave TLA+ alone, I think its support for sets is sufficient.

Comments URL: https://news.ycombinator.com/item?id=12024392

Points: 3

# Comments: 0

Back in Sydney now some two years. I don't have the receipt or any record of the purchase. When i phoned Apple, they wouldn't help, said I wasn't the registered owner.

But what really pissed me off was that they wouldn't even reach out to that owner. So I'm stuck.

As a family, we've purchased our fair share of Apple hardware over the past 7 years or so, you name it, we probably have at least one.

Not any more.