What LaTeX package does one use to get the "back" link at the end of footnotes like the linked PDF exhibits?
hyperref does this with the "\ref{}" command, it can link to any defined \label
The Future of TLA+ [pdf]
51–60 of 107 posts
Re: The Future of TLA+ [pdf]
#52> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…
> "specification of system behavior" sounds like a programming language to me. A systems programming language, even. Lamport has directly and repeatedly addressed the differences between what's desirable in a specification language versus what's desirable in a programming language. Understanding the difference is vital to writing specifications.
I looked for this "direct address". All I can tell is that he's repeatedly contradicted himself. http://lambda-the-ultimate.org/node/4922#comment-79370
Re: The Future of TLA+ [pdf]
#53Earlier quoted context omitted.
I mean the zero function, i.e., the one that is zero everywhere, because if y ∈ ℤ and y = -y, then y = 0.
Doesn't ℤ include negative natural numbers? * Nevermind, I just saw you used the ">" sign in the definition. Is it why the definition only applies to positive numbers? In any case, you did not write it in your textual description, which looked confusing to me. I think it would be easier if one could define it as ℤ+ or something like that.
The original from pron:
f ≜ CHOOSE f ∈ [Int → Int] :
∀ x ∈ Int : f[x] = -f[x]
Re: The Future of TLA+ [pdf]
#54I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before. I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software. It really is just ma…
I'd suggest starting with P (https://github.com/p-org/P), or picking up Hillel Wayne's TLA+ book to get started.
Re: The Future of TLA+ [pdf]
#55Earlier quoted context omitted.
TLA+ is executable in the sense of Prolog: there is an algorithm (the TLA+ implementation) that takes a TLA+ program and produces output. Most mathematics is not executable in this sense, you will have a very difficult time doing anything useful with the PDF's of published math papers. Math is a natural language, TLA+ is not. And I would agree, TLA+ as a specification is different from TLA+ as an implementation. I ge…
> Math is a natural language Almost spit out my drink dude, no jokes this early in the day.
ChatGPT does just fine with math. I wasn't joking...
Re: The Future of TLA+ [pdf]
#56Earlier quoted context omitted.
Doesn't ℤ include negative natural numbers? * Nevermind, I just saw you used the ">" sign in the definition. Is it why the definition only applies to positive numbers? In any case, you did not write it in your textual description, which looked confusing to me. I think it would be easier if one could define it as ℤ+ or something like that.
The original from pron: f ≜ CHOOSE f ∈ [Int → Int] : ∀ x ∈ Int : f[x] = -f[x] You added the > in your quote of pron, he didn't have it in the original. There is no c in ℤ with c != 0 s.t. f(x) = c and f(x) = -f(x), that would imply that c = -c for non-zero integers which is not true. The only function that can satisfy pron's constraints is f(x) = 0 since c = 0 is the only time c = -c, or 0 = -0.
That’s true, my mistake. Thank you for the clarification! In this case, I have another question.
Why is this original definition different than say
f ≜ CHOOSE f ∈ [Int → Int]:
∀ x ∈ Int : f[x] = 0
Re: The Future of TLA+ [pdf]
#57I was looking at TLA a few months ago to consider what it would take to prove multiregion fail over worked correctly. Considering I'd never looked at it before. I did not find it straight forwardly grokkable, which makes me sad. Maybe it needs a library of axioms? I feel there's probably a very nice way to work through it without ingesting effectively a graduate school course in proving software. It really is just ma…
https://lamport.azurewebsites.net/video/videos.html is really excellent
Re: The Future of TLA+ [pdf]
#58Earlier quoted context omitted.
I wouldn't say it's a TLA+ alternative because it cannot do the most powerful and useful things TLA+ does (esp. refinement), but it is an alternative for programmers who just want to specify at a level that closer to code and model-check specifications.
Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+." Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement. Shoutout to operator labels.
So for us normies does that mean skip TLA?
Re: The Future of TLA+ [pdf]
#59As someone who's fascinated by formal verification and who's early in their career, what advice do senior folks who have been using TLA+ have? TLA+ isn't taught in most universities and while I've read about so many interesting applications, I'm yet to convince myself that someone would hire me for knowing it rather than just teaching it to me on the job. Any tips to get started would also be appreciated!
There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.
>There's very little tech that somebody is going to hire you for knowing. It's a tool like many others.
I guess this must be true on places like SF since I see this so often on HN, but almost every single job listing I've seen strictly requires knowledge of a specific tech stack, with the exception of a few internship programs.
Re: The Future of TLA+ [pdf]
#60I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib ( https://github.com/leanprover-community/mathlib4 ). What’s so great about the experience of using Lean is that I can pull theorems off the shelf from Mathlib, use them if I want to, or learn from the way their proofs work if I want to do something similar. > The reas…
I loved the concept of TLA+ and tried to get into it, but as you say
> The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language
the syntax was very non-standard which was off putting, and the expected dev ux seemed to be of the 'get it right on paper first then just write the text' variety. This was also off putting and I think you're right that there is a space for making a DX focused TLA+ transpiled language