ahelwer

Punters with enough good boy points were rolling into very obscure and technical tags to close questions as duplicate (they weren't). When I saw how impossible it was for people to ask questions in a tag I was an expert in I knew the site was cooked. Imagine, like, giving physiotherapy forum power users moderator privileges on HN.

Nothing is yet proven and other articles have painted this arrest as shocking.

I've stopped watching all sports because of this. You can't even talk about sports online now without some dull punter whining that their parlay didn't hit. It's nauseating. The gambling industry produces no value.

Unfortunately it is. Thought the whole thing was a scam until six months ago. I think pretty highly of my development skills and have to be objective and admit I am outclassed in debugging and operational tasks now (and it isn't close). Writing non-script code isn't quite there yet (they are bad at abstraction) but I can't confidently predict how much longer that will be the case.

Interesting that they have a camera behind the TV, I suppose for this exact purpose.

I hope you are right but fear the reality might be more similar to Elysium, if not intentional depopulation. This is straying far into sci-fi but it might come down to whether AI escapes control of the ruling class and whether it is benevolent or not. The future looks like rule by those with money to fund the manufacture of robotic armies, if not.

There is a lot of that to be sure, but the bridge to a world where meals & health are not sustained through toil is completely missing. Hence the dark joking about escaping the permanent underclass. Nobody in any position of power is even hinting this is driving toward post-scarcity. It just looks like the same old vile maxim, all for ourselves, and nothing for other people.

I like Wolfram and always enjoy reading his posts. An irreconcilable thing here is Wolfram clearly wants the Mathematica language to be central to the development of math as a field, but it's proprietary and so there is no guarantee it will survive the dissolution of the company if/when that happens. With Lean & others you can fairly safely assume that a particular version will be archived somewhere, and so a proof formalized for that version can be checked at any time. Not so with Mathematica. It's unfortunate, Mathematica is a cool language, but that's just the structure of incentives at this time. This is without getting into what a proof formalized in Mathematica would even mean, the relative maturity of the kernel and the possibility of there being multiple kernel implementations for cross-checking, and so on.

Many TLA+ users will tell you the greatest value of writing a spec was it forced them to think clearly about their system. However, thinking is very hard to sell, so we tend to center the razzle-dazzle about model-checking properties of your state space. Which is a great capability, don't get me wrong! Most non-trivial systems have a state space far larger than can be assessed for finding bugs via thinking.

It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.

I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.

You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.

A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.

Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.

This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.

I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.

Unfortunately a lot of us will die in comparable ways if we are lucky enough to get that old. My grandmother was healthy & mentally with it until stroking out in her garden one day at the age of 90. That is the best any of us can hope for and the reality will almost certainly be far more painful and prolonged.