6 ms·

> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification

by pron 11mo ago

> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many possible programs or even magical oracles that can do what a program does). To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed.

goryDeets 11mo ago
[dead]
anon-3988 11mo ago
> To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed. Do you really think it is going to be easier for the average developer to write a specification for their program that does not terminate vs Giving them a framework or a language that does not have for loop? Edit: If by formal verification you mean type checking. That I very much agree.
- DennisP 11mo ago
  Maybe it's difficult for the average developer to write a formal specification, but the point of the article is that an AI can do it for them.
nyrikki 11mo ago
TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Usually you can abstract them out, but if you absolutely need floats then TLA+ is the wrong tool for the job. TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. [0] https://learntla.com/core/operators.html https://learntla.com/core/operators.html
- nextos 11mo ago
  There are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see e.g. what PRISM [1] and Storm [2] implement. That is not within the scope of TLA+. Formal methods are really broad, ranging from lightweight type systems to theorem proving. Some techniques are fantastic for one type of problem but fail at others. This is quite natural, the same thing happens with different programming paradigms. For example, what is adequate for a hard real-time system (timed automata) is useless for a typical CRUD application. [1] https://www.prismmodelchecker.org https://www.prismmodelchecker.org [2] https://www.stormchecker.org https://www.stormchecker.org
  - hwayne 11mo ago
    I really do wish that PRISM can one day add some quality of life features like "strings" and "functions" (Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)
- pron 11mo ago
  > You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” You really don't. It's not LTL. Abstraction/refinement relations are at the core of TLA. > Or even floats [0] and it becomes challenging and strings are a mess. No problem with floats or strings as far as specification goes. The particular verification tools you choose to run on your TLA+ spec may or may not have limitations in these areas, though. > TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. TLA+ can specify anything that could be specified in mathematics. That there is no predefined set of floats is no more a problem than the one physicists face because mathematics has no "built-in" concept for metal or temperature. TLA+ doesn't even have any built in notions of procedures, memory, instructions, threads, IO, variables in the programming sense, or, indeed programs. It is a mathematical framework for describing the behaviour of discrete or hybrid continuous-discrete dynamical systems, just as ODEs describe continuous dynamical systems. But you're talking about the verfication tools you can run on TLA+ spec, and like all verification tools, they have their limitations. I never claimed otherwise. You are, however, absolutely right that it's difficult to specify probabilistic properties in TLA+.
eru 11mo ago
What you said certainly works, but I'm not sure computability is actually the biggest issue here? Have a look at how SAT solvers or Mixed Integer Linear Programming solvers are used. There you specify a clear goal (with your code), and then you let the solvers run. You can, but you don't need to, let the solvers run all the way to optimality. And the solvers are also allowed to use all kinds of heuristics to find their answers, but that doesn't impact the statement of your objective. Compare that to how many people write code without solvers: the objective of what your code is trying to achieve is seldom clearly spelled out, and is instead mixed up with the how-to-compute bits, including all the compromises and heuristics you make to get a reasonable runtime or to accommodate some changes in the spec your boss asked for at the last minute. Using a solver ain't formal verification, but it shows the same separation between spec and implementation. Another benefit of formal verification, that you already imply: your formal verification doesn't have to determine the behaviour of your software, and you can have multiple specs simultaneously. But you can only have a single implementation active at a time (even if you use a high level implementation language.) So you can add 'handling a user request must terminate in finite time' as a (partial) spec. It's an important property, but it tells you almost nothing about the required business logic. In addition you can add "users shouldn't be able to withdraw more than they deposited" (and other more complicated rules), and you only have to review these rules once, and don't have to touch them again, even when you implement a clever new money transfer routine.
mrkeen 11mo ago
Can TLA+ prove anything about something you specify but don't execute?
- igornotarobot 11mo ago
  TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof system that can automate some proof steps by delegating to SMT solvers: https://proofs.tlapl.us/doc/web/content/Home.html https://proofs.tlapl.us/doc/web/content/Home.html - Apalache is the symbolic model checker that delegates verification to Z3. It can prove properties without executing anything, or rather, executing specs symbolically. For instance, it can do proofs via inductive invariants but only for bounded data structures and unbounded integers. https://apalache-mc.org/ https://apalache-mc.org/ - Finally, TLC is an enumerative model checker and simulator. It simply produces states and enumerates them. So it terminates only if the specification produces a finite number of states. It may sound like executing your specification, but it is a bit smarter, e.g., when checking invariants it will never visit the same state twice. This gives TLC the ability to reason about infinite executions. Confusingly, TLC does not have its own page, as it was the first working tool for TLA+. Many people believe that TLA+ is TLC: https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus
  - pron 11mo ago
    > It may sound like executing your specification, but it is a bit smarter, It's more than just "a bit smarter" I would say, and explicit state enumeration is nothing at all like executing a spec/program. For example, TLC will check in virtually zero time a spec that describes a nondeterministic choice of a single variable x being either 0 or 1 at every step (as there are only two states). The important aspect here isn't that each execution is of infinite length, but that there are an uncountable infinity of behaviours (executions) here. This is a completely different concept from execution, and it is more similar to abstract interpretation (where the meaning of a step isn't the next state but the set of all possible next states) than to concrete interpretation.
- 11mo ago
avmich 11mo ago
Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.
- atakan_gurkan 11mo ago
  This sounds very interesting. Do you have a reference?
  - avmich 11mo ago
    Saw something like that once, couldn't find recently, sorry. Ask Peter?..
- pron 11mo ago
  Writing in a language that guarantees termination is not very interesting in itself, as every existing program could automatically be translated into a non-Turing-complete language where the program is proven to terminate, yet behaves exactly the same: the language is the same as the original, only loops/rectursion ends the program after, say, 2^64 iterations. This, in itself, does not make programs any easier to analyse. In fact, a language that only has boolean variables, no arrays, no recursion, and loops of depth 2 at most is already instractable to verify. It is true that programs in Turing-complete languages cannot generally be verified in efficiently, but most non-Turing-complete languages also have this property. Usually, when we're interested in termination proofs, what we're really interested in is a proof that the algorithm makes constant progress that converges on a solution.
  - avmich 11mo ago
    I think the interesting progress in programs can generally be achieved for many programs, which take input and produce output and then terminate. For servers, which wait for requests, the situation seem to be different.

by pron 11mo ago

goryDeets 11mo ago

[dead]

anon-3988 11mo ago

> To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed. Do you really think it is going to be easier for the average developer to write a specification for their program that does not terminate vs Giving them a framework or a language that does not have for loop? Edit: If by formal verification you mean type checking. That I very much agree.

DennisP 11mo ago
Maybe it's difficult for the average developer to write a formal specification, but the point of the article is that an AI can do it for them.

nyrikki 11mo ago

TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Usually you can abstract them out, but if you absolutely need floats then TLA+ is the wrong tool for the job. TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. [0] https://learntla.com/core/operators.html https://learntla.com/core/operators.html

nextos 11mo ago
There are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see e.g. what PRISM [1] and Storm [2] implement. That is not within the scope of TLA+. Formal methods are really broad, ranging from lightweight type systems to theorem proving. Some techniques are fantastic for one type of problem but fail at others. This is quite natural, the same thing happens with different programming paradigms. For example, what is adequate for a hard real-time system (timed automata) is useless for a typical CRUD application. [1] https://www.prismmodelchecker.org https://www.prismmodelchecker.org [2] https://www.stormchecker.org https://www.stormchecker.org
- hwayne 11mo ago
  I really do wish that PRISM can one day add some quality of life features like "strings" and "functions" (Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)
pron 11mo ago
> You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” You really don't. It's not LTL. Abstraction/refinement relations are at the core of TLA. > Or even floats [0] and it becomes challenging and strings are a mess. No problem with floats or strings as far as specification goes. The particular verification tools you choose to run on your TLA+ spec may or may not have limitations in these areas, though. > TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. TLA+ can specify anything that could be specified in mathematics. That there is no predefined set of floats is no more a problem than the one physicists face because mathematics has no "built-in" concept for metal or temperature. TLA+ doesn't even have any built in notions of procedures, memory, instructions, threads, IO, variables in the programming sense, or, indeed programs. It is a mathematical framework for describing the behaviour of discrete or hybrid continuous-discrete dynamical systems, just as ODEs describe continuous dynamical systems. But you're talking about the verfication tools you can run on TLA+ spec, and like all verification tools, they have their limitations. I never claimed otherwise. You are, however, absolutely right that it's difficult to specify probabilistic properties in TLA+.

eru 11mo ago

What you said certainly works, but I'm not sure computability is actually the biggest issue here? Have a look at how SAT solvers or Mixed Integer Linear Programming solvers are used. There you specify a clear goal (with your code), and then you let the solvers run. You can, but you don't need to, let the solvers run all the way to optimality. And the solvers are also allowed to use all kinds of heuristics to find their answers, but that doesn't impact the statement of your objective. Compare that to how many people write code without solvers: the objective of what your code is trying to achieve is seldom clearly spelled out, and is instead mixed up with the how-to-compute bits, including all the compromises and heuristics you make to get a reasonable runtime or to accommodate some changes in the spec your boss asked for at the last minute. Using a solver ain't formal verification, but it shows the same separation between spec and implementation. Another benefit of formal verification, that you already imply: your formal verification doesn't have to determine the behaviour of your software, and you can have multiple specs simultaneously. But you can only have a single implementation active at a time (even if you use a high level implementation language.) So you can add 'handling a user request must terminate in finite time' as a (partial) spec. It's an important property, but it tells you almost nothing about the required business logic. In addition you can add "users shouldn't be able to withdraw more than they deposited" (and other more complicated rules), and you only have to review these rules once, and don't have to touch them again, even when you implement a clever new money transfer routine.

mrkeen 11mo ago

Can TLA+ prove anything about something you specify but don't execute?

igornotarobot 11mo ago
TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof system that can automate some proof steps by delegating to SMT solvers: https://proofs.tlapl.us/doc/web/content/Home.html https://proofs.tlapl.us/doc/web/content/Home.html - Apalache is the symbolic model checker that delegates verification to Z3. It can prove properties without executing anything, or rather, executing specs symbolically. For instance, it can do proofs via inductive invariants but only for bounded data structures and unbounded integers. https://apalache-mc.org/ https://apalache-mc.org/ - Finally, TLC is an enumerative model checker and simulator. It simply produces states and enumerates them. So it terminates only if the specification produces a finite number of states. It may sound like executing your specification, but it is a bit smarter, e.g., when checking invariants it will never visit the same state twice. This gives TLC the ability to reason about infinite executions. Confusingly, TLC does not have its own page, as it was the first working tool for TLA+. Many people believe that TLA+ is TLC: https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus
- pron 11mo ago
  > It may sound like executing your specification, but it is a bit smarter, It's more than just "a bit smarter" I would say, and explicit state enumeration is nothing at all like executing a spec/program. For example, TLC will check in virtually zero time a spec that describes a nondeterministic choice of a single variable x being either 0 or 1 at every step (as there are only two states). The important aspect here isn't that each execution is of infinite length, but that there are an uncountable infinity of behaviours (executions) here. This is a completely different concept from execution, and it is more similar to abstract interpretation (where the meaning of a step isn't the next state but the set of all possible next states) than to concrete interpretation.
11mo ago

avmich 11mo ago

Peter Norvig once proposed to consider a really large grammar, with trillion rules, which could simulate some practically small applications of more complex systems. Many programs in practice don't need to be written in Turing-complete languages, and can be proven to terminate.

atakan_gurkan 11mo ago
This sounds very interesting. Do you have a reference?
- avmich 11mo ago
  Saw something like that once, couldn't find recently, sorry. Ask Peter?..
pron 11mo ago
Writing in a language that guarantees termination is not very interesting in itself, as every existing program could automatically be translated into a non-Turing-complete language where the program is proven to terminate, yet behaves exactly the same: the language is the same as the original, only loops/rectursion ends the program after, say, 2^64 iterations. This, in itself, does not make programs any easier to analyse. In fact, a language that only has boolean variables, no arrays, no recursion, and loops of depth 2 at most is already instractable to verify. It is true that programs in Turing-complete languages cannot generally be verified in efficiently, but most non-Turing-complete languages also have this property. Usually, when we're interested in termination proofs, what we're really interested in is a proof that the algorithm makes constant progress that converges on a solution.
- avmich 11mo ago
  I think the interesting progress in programs can generally be achieved for many programs, which take input and produce output and then terminate. For servers, which wait for requests, the situation seem to be different.