3 ms·

> It is immediately obvious that TLA+ is simpler than SML, yet as powerful as Coq What facilities for data abstraction does TLA+ have? How do I hide the repres

> It is immediately obvious that TLA+ is simpler than SML, yet as powerful as Coq What facilities for data abstraction does TLA+ have? How do I hide the representational choices of a module whose internal implementation I'm not currently concerned with? > it is TLA+ that requires little more than high school math. You can reason with it about any kind of algorithm you like, using the same simple, familiar math (FOL, ZF First-order logic is not “high-school math”. You can't expect most high schoolers to know how to correctly manipulate logical quantifiers. (Of course, a competent programmer should know, but that doesn't mean one should force themselves to use a more complicated tool when a simpler one is available.) And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. Have you ever seen the crazy things that Harvey Friedman does with large cardinals? > plus three temporal operators, of which only one is really used for safety properties). That's the thing: I want to reason in a time-independent manner as much as possible. Time-invariant reasoning is simpler and mathematically more beautiful than exploring state spaces alongside with your processes. > In TLA+ there is no such thing as an imperative or a functional program. (...) E.g., in TLA+, all algorithms (...) denote a set of behaviors, where each behavior is an infinite sequence of states. Then in TLA+ all algorithms are expressed as imperative programs. > Think of algorithms as abstract state machines, and reasoning becomes -- if not simple -- then as simple as possible (today, at least). By virtue of exploring large state spaces? > But the proof works on the representation of the program, which is just a logical predicate. Which is it? (0) Two programs that compute the same result, but have different efficiency characteristics, are represented as logically (not just syntactically) different predicates. (1) You don't distinguish between programs that compute the same result, but have different efficiency characteristics. The former is unusable as a basis for reasoning about extensional equality. The latter is unusable as a basis for reasoning about complexity. > Yes. First I thought of it, then I wrote it, then I added details until it checked. Checked by whom? > But let me tell you: if a proof assistant would ever make proofs easier than doing them in your head, then I'd be very happy. Usually they make things harder because they need lots of detail. I don't disagree with this one. > But, unfortunately, proof assistants don't help you uncover a proof. Model checkers can do that sometimes. Type inference reconstructs type derivations all of the time. Reliably. Of course, those type derivations are all boring routine, but it means that human programmers themselves aren't burdened with it.

pron 10y ago
> What facilities for data abstraction does TLA+ have? The full strengths of set theory (sets, functions), plus sugar for sequences and records. > How do I hide the representational choices of a module I'm not currently concerned with? TLA+ has a simple module system. Definitions can be local or public. > First-order logic is not “high-school math”. You can't expect most high schoolers to know how to correctly manipulate logical quantifiers. Depends on the country I guess. But OK, first year college. > And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. None of that has any bearing on specifying algorithms, though. > That's the thing: I want to reason in a time-independent manner as much as possible. Time-invariant reasoning is simpler and mathematically more beautiful than exploring state spaces alongside with your processes. That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+. > Then in TLA+ all algorithms are expressed as imperative programs. No. They're expressed as nondeterministic abstract state machines, written as a first order logic predicate. Each step of the machine is arbitrarily complex. You can specify a program in TLA+ that in each step solves a difficult SAT problem, or even the halting problem. Imperative is an attribute of a programming language with programming language semantics; TLA+ is ordinary math and doesn't have any of those attributes. It's like saying that calculus is imperative. However, it certainly isn't functional because it doesn't identify the concept of a function with the concept of a computation. I guess you could specify a functional program as a machine that computes its result in a single state (although I wouldn't). You could then model, I don't know, LLVM machine code, and shoe that the machine code algorithm is a refinement of the functional program. > By virtue of exploring large state spaces? I don't understand the question. The reasoning -- as any other formal reasoning -- is done by manipulating logical formulas. The state space is a property of the model, not of the logic. > Checked by whom? TLAPS, the TLA+ proof system. > Type inference reconstructs type derivations all of the time. It's done reliably because the properties they represent are kept very computationally simple. In TLAPS uses SMT solvers to reduce the effort, and where a type would be inferred, so would a proposition. The problem is with more interesting propositions.
- catnaroek 10y ago
  > The full strengths of set theory (sets, functions), plus sugar for sequences and records. Set theory doesn't have any facilities for data abstraction. If anything, it's the antithesis of data abstraction: every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes. > TLA+ has a simple module system. Hierarchical modules? Parameterized module families? Multiple views of the same module, showing or hiding different aspects of it? I use this stuff everyday not only to keep my programs modular, but also to keep their proofs of correctness modular. >> And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. > None of that has any bearing on specifying algorithms, though. You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that. > That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+. If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free. > It's done reliably because the properties they represent are kept very computationally simple. That's a feature. It helps you delimit the routine stuff (and can be reliably verified mechanically, and should be most of your program, if it's designed sensibly) from what requires creativity to prove. That being said, of course, existing type systems don't automatically verify everything that could be considered “routine”, so this is an area where further improvement is necessary. > The problem is with more interesting propositions. Prove them by hand. Good old-fashioned brain usage is never going away. --- By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof?

pron 10y ago

> What facilities for data abstraction does TLA+ have? The full strengths of set theory (sets, functions), plus sugar for sequences and records. > How do I hide the representational choices of a module I'm not currently concerned with? TLA+ has a simple module system. Definitions can be local or public. > First-order logic is not “high-school math”. You can't expect most high schoolers to know how to correctly manipulate logical quantifiers. Depends on the country I guess. But OK, first year college. > And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. None of that has any bearing on specifying algorithms, though. > That's the thing: I want to reason in a time-independent manner as much as possible. Time-invariant reasoning is simpler and mathematically more beautiful than exploring state spaces alongside with your processes. That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+. > Then in TLA+ all algorithms are expressed as imperative programs. No. They're expressed as nondeterministic abstract state machines, written as a first order logic predicate. Each step of the machine is arbitrarily complex. You can specify a program in TLA+ that in each step solves a difficult SAT problem, or even the halting problem. Imperative is an attribute of a programming language with programming language semantics; TLA+ is ordinary math and doesn't have any of those attributes. It's like saying that calculus is imperative. However, it certainly isn't functional because it doesn't identify the concept of a function with the concept of a computation. I guess you could specify a functional program as a machine that computes its result in a single state (although I wouldn't). You could then model, I don't know, LLVM machine code, and shoe that the machine code algorithm is a refinement of the functional program. > By virtue of exploring large state spaces? I don't understand the question. The reasoning -- as any other formal reasoning -- is done by manipulating logical formulas. The state space is a property of the model, not of the logic. > Checked by whom? TLAPS, the TLA+ proof system. > Type inference reconstructs type derivations all of the time. It's done reliably because the properties they represent are kept very computationally simple. In TLAPS uses SMT solvers to reduce the effort, and where a type would be inferred, so would a proposition. The problem is with more interesting propositions.

catnaroek 10y ago
> The full strengths of set theory (sets, functions), plus sugar for sequences and records. Set theory doesn't have any facilities for data abstraction. If anything, it's the antithesis of data abstraction: every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes. > TLA+ has a simple module system. Hierarchical modules? Parameterized module families? Multiple views of the same module, showing or hiding different aspects of it? I use this stuff everyday not only to keep my programs modular, but also to keep their proofs of correctness modular. >> And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. > None of that has any bearing on specifying algorithms, though. You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that. > That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+. If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free. > It's done reliably because the properties they represent are kept very computationally simple. That's a feature. It helps you delimit the routine stuff (and can be reliably verified mechanically, and should be most of your program, if it's designed sensibly) from what requires creativity to prove. That being said, of course, existing type systems don't automatically verify everything that could be considered “routine”, so this is an area where further improvement is necessary. > The problem is with more interesting propositions. Prove them by hand. Good old-fashioned brain usage is never going away. --- By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof?