Just saw Hillel Wayne link to Quint on LinkedIn, and I finally want to try writing TLA+ as a result... https://quint-lang.org/docs/lang

Since this was linked to from here, I assume this is likely to be something I’m interested in. But after a few minutes poking around the documentation, I did not find anything about what this is, what problems it solves, what it does differently, or really much of anything like that. I made a bug report about the documentation, but if you know the creator, you might mention this.

It's a syntax built on top of TLA+, which is a version of TLA (Temporal Logic of Actions), which is a logic-based language for encoding software designs and using logic solving to determine if they satisfy design specifications.

Can one also use it for regular programming?

Not general purpose, no. E.g. there is no way to find a substring in a string.