Re:Haskell Problems for a New Decade
by pron on Sunday January 26, 2020 @02:49PM
(#22154285)
> TLA+ wasn't the first (Z was earlier)
Was Z ever used outside high-assurance software (or the classroom)? BTW, while Z certainly employs a formal logic, I don't think it is a formal logic itself -- unlike TLA+ -- at least not in the common usage of the term.
> TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
But for a high-profile company to write about it, it first had to be used at that high-profile company for some mainstream software. My point is that being an accessible logic may not be a sufficient condition for adoption, but it is certainly a necessary one, and an extraordinary accomplishment. Both Isabelle and Coq have had some significant exposure, and yet they are still virtually unused by non-researchers or former researchers.
> When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling.You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
Maybe, but "listening to feedback" is not the same as accepting it at face value. The vast majority of those people were either relative beginners or not even that. To understand the feedback I need to first make sure they understand what TLA+ is and how it's supposed to be used, or else their very expectations could be misplaced. I've written my thoughts on why I thought the answer to that question is negative here: https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest... I don't make any decisions whatsoever on TLA+'s development, so I'm not the one who needs convincing, but as far as forming my personal opinion on the feedback, what I wrote there is my response to it. It's certainly possible that either my premise or my conclusion is wrong, or both. It's also possible that both are right, and still better CLI support should be a top priority. That is why I would very much like to understand the feedback in more depth. If you like, we could continue it on /r/tlaplus (or the mailing list), where it will be more easily discoverable.
> I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Sure, but the question is, is that the most important thing to focus efforts on? Anyway, I'm sure that any contribution that makes any part of the TLA+ toolset more friendly, even if for a subset of users, would be welcomed and appreciated by the maintainers, as long as it doesn't interfere with what they consider more important goals.
Was Z ever used outside high-assurance software (or the classroom)? BTW, while Z certainly employs a formal logic, I don't think it is a formal logic itself -- unlike TLA+ -- at least not in the common usage of the term.
> TLA+'s success has much less to do with anything especially accessible about it and more because a high profile company wrote about it.
But for a high-profile company to write about it, it first had to be used at that high-profile company for some mainstream software. My point is that being an accessible logic may not be a sufficient condition for adoption, but it is certainly a necessary one, and an extraordinary accomplishment. Both Isabelle and Coq have had some significant exposure, and yet they are still virtually unused by non-researchers or former researchers.
> When I asked "what would make TLA+ easier to use", tons of people mentioned better CLI tooling.You told them all that they don't actually need that and they are thinking about TLA+ wrong. Maybe you aren't actually listening to the feedback.
Maybe, but "listening to feedback" is not the same as accepting it at face value. The vast majority of those people were either relative beginners or not even that. To understand the feedback I need to first make sure they understand what TLA+ is and how it's supposed to be used, or else their very expectations could be misplaced. I've written my thoughts on why I thought the answer to that question is negative here: https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest... I don't make any decisions whatsoever on TLA+'s development, so I'm not the one who needs convincing, but as far as forming my personal opinion on the feedback, what I wrote there is my response to it. It's certainly possible that either my premise or my conclusion is wrong, or both. It's also possible that both are right, and still better CLI support should be a top priority. That is why I would very much like to understand the feedback in more depth. If you like, we could continue it on /r/tlaplus (or the mailing list), where it will be more easily discoverable.
> I've also heard it from tons of experienced TLA+ users that they'd like better CLI tooling.
Sure, but the question is, is that the most important thing to focus efforts on? Anyway, I'm sure that any contribution that makes any part of the TLA+ toolset more friendly, even if for a subset of users, would be welcomed and appreciated by the maintainers, as long as it doesn't interfere with what they consider more important goals.