6 ms·
> Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation prog
by pron 2y ago
> Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages.
Yeah, but in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Programming languages of every generation are very useful, as is mathematics, even though they're not the same thing.
> More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases.
Coq and Idris are very different in the way they're typically used, and I'd say TLA+ is much closer to Coq than to Idris (and is probably more popular than the two combined), but to "execute" anything the specification needs to be at a certain level that's detailed enough to produce a program, and oftentimes that is very much not what you want.
It would be extremely useful to have a language that you could describe the various properties of a car and it would compile your specification into the design of a car (you would need to give it sufficient detail as there are choices to be made). But it would also be extremely useful to have a language that could be used to learn certain things about a car -- say, it's braking distance -- without specifying it in sufficient detail to actually build one. That is what maths is good for -- describing things at arbitrary levels of detail to answer relevant questions.
For example, you may have a 5 MLOC distributed system, and you want to know if a certain kind of failure may lead to data loss. You could use TLA+ to describe just the relevant details to answer the question in, say, 200 lines of formulas. That you cannot compile those formulas into a working 5 MLOC piece of software is not a downside of mathematics, but rather the point.
> TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be
And because it's not a language for programming but a language for mathematics, so it looks and feels pretty close to plain mathematics (only it's formal), as that's the obvious choice for writing mathematics.
- Mathnerd314 2y ago> in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Well, in TLA+ you can write programs that run forever (or at longer than you'll live) and don't do anything like "model check" or whatever you want to call executing TLA+, even though they are perfectly sound mathematically. This should make it clear that TLA+ is not maths.
- auggierose 2y agoProving the Riemann hypothesis might also take longer than you live, and in fact may be impossible. So the Riemann hypothesis is not math?
- pron 2y agoI don't understand the order of your implication. You can use maths (say, some ZFC formalism) to specify the execution of any Python or Java or C program and even write a software tool that executes it. It's the converse that isn't true: You cannot write a Python or Java or C program that accurately expresses many mathematical theorems (e.g. you can only express computable numbers in a program). I.e. the expressivity of mathematics includes that of programming, but not vice versa. In TLA+ you can express every theorem in ZFC, but that doesn't mean you can automatically prove or disprove every proposition or even every theorem, because that is indeed a limitation of mathematics. There are also lots and lots of theorems you can state and prove in TLA+ yet not prove automatically with the TLC model-checker (or, indeed, with any known automatic proof method). That is a limitation of TLC (or of any known automatic proof methods), but not one of TLA+.
- Mathnerd314 2y agoActually the converse is true: Lean and other projects have formalized most mathematical theorems. But it is an "additive" process - it is easy to paraphrase a formal Lean theorem as colloquial mathematics, but it is hard to formalize colloquial mathematics in Lean. Some of this is due to Lean not being as developed as it could be, but also there is simply that some "theorems" in mathematics are simply "wrong" in that they make unstated assumptions and handwave away important parts of the proof. It is in this sense that programming is less expressive than mathematics, in that you can get away with writing things in mathematics that you can't get through a theorem checker. And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics. The lack of these limitations is what I would say the limitation of mathematics is, that even well-known proofs are not necessarily completely "true" due to unstated assumptions. Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc. When you say "prove" a TLA+ program I first thought this was formally checking it with TLC / TLAPS / etc. But it seems you have a different notion of proof, some sort of handwaving "it looks right" notion. From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it. You might as well say "You can express every theorem in ZFC in Java by writing it in a comment" - it is not an informative observation. The interesting TLA+ programs are the ones that can be checked with TLC / TLAPS / etc., and to the extent one can work with these programs programmatically, TLA+ is a programming language.