4 ms·

I don't know that much about it, but the impression I got from studying TLA+ was that machine-executable code was distinctly not mathematics, and that programs

I don't know that much about it, but the impression I got from studying TLA+ was that machine-executable code was distinctly not mathematics, and that programs are never provable. Am I wrong? Or is this just the kind of sensational snake-oil that HN readers are susceptible to buying.

bluGill 3y ago
Most code is so complex that even with the aid of a computer we couldn't run a proof on it if we tried. Most (all!) code also has bugs so if we tried to prove it we would instead prove it doesn't meet requirements. However the theory itself allows that all code could be mathematically proven if you can work around those two issues. It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.
- staunton 3y ago
  > hardware is a lot more likely to be mathematically proven Maybe that's a nitpick, but I would say it's fundamentally impossible to mathematically prove anything at all about a physical system. You have to assume some model to do the proof and have no way of ever "proving" (what would that even mean?) that model. I guess you're referring to the fact that verification and formal methods are used in hardware more often than software. This is due to commercial reasons: you can't just reprogram a million chips once they leave your fab.
- Tainnor 3y ago
  We run proofs on code all the time, it's called type-checking. What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.
- kaba0 3y ago
  > However the theory itself allows that all code could be mathematically proven I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.
  - bluGill 3y ago
    But we never need to prove the general case, only specific cases. The general case includes an infinite number of inputs, but in reality there is only a finite number of states a physical computer can have (the number of states far exceeds the number of atoms in the universe, but it is still finite)
    - alpaca128 3y ago
      I don't think a theoretical computer scientist would agree.
      - bluGill 3y ago
        So long as the number of states is finite theory says we can prove by exhaustion. Either a state terminates, or it becomes a different state. Then you do a tree seach until you have reached a termination or a state already in the tree. You need more memory than the number of states to do this, but theroy allows for infine memory in the proof.
        bluGill 3y ago
        Remember the halting problem is proving within a system, we can often step outside the system to prove it. Which sometimes allowes for more properties to be proved'
        drdeca 3y ago
        The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.) Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.
aeneasmackenzie 3y ago
Typical proofs don’t cover side channels, just ISA semantics. With the big asterisk that most programs are running on top of an unverified kernel on an unverified machine-level blob on an unverified ISA implemented by an unverified chip, you can absolutely prove the behavior of programs. Lamport has an unusual attitude towards verification and comes towards it from a slightly different angle, and model checking is not a good approach to machine-level proofs.
staunton 3y ago
What does it mean to say "a program is provable"? You have to prove something about it. In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.
miloignis 3y ago
If I understand what you are asking about correctly, then I do think you are mistaken. As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done. This ranges from things like CakeML (https://cakeml.org/ https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages. Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.
mapM 3y ago
I think you misunderstand. On your point about programs not being "provable": it is certainly possible to prove some properties about some programs. It is not necessarily easy, and it very much depends on the program and the property in question, but it is possible. However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.
- nyrikki 3y ago
  Entscheidungsproblem, the Halting problem, the total function problem, etc... typically relate to arbitrary programs. The point being is there is no single general algorithm that can solve them. The example you gave above is propositional logic, or zeroith order logic which is known to be decidable. First order logic and higher order logic are not decidable. Total functions are also not subject to the halting problem, but unfortunately finding a total function in the general case is also undecidable.
  - deterministic 3y ago
    It doesn’t matter. What matters is if you can prove things you care about true for code you care about. And yes we can prove termination and zero bugs for a lot of practical useful code. Examples: seL4 is a proven correct micro kernel and CompCert is a proven correct C compiler. The trick is to use programming languages that are total i.e. not general infinite tape turing machines.
nyrikki 3y ago
Note this quote from the article. "One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox." This is similar to constraints of making something semi-decidable or recursively enumerable. Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways. Some things are easier to find in type theory, other in set theory and for some Turing machines work better. The Church–Turing thesis isn't provable but is the safe assumption. IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory. As an example related to term rewriting which will be important to ML. https://arxiv.org/abs/2307.14805 https://arxiv.org/abs/2307.14805

bluGill 3y ago

Most code is so complex that even with the aid of a computer we couldn't run a proof on it if we tried. Most (all!) code also has bugs so if we tried to prove it we would instead prove it doesn't meet requirements. However the theory itself allows that all code could be mathematically proven if you can work around those two issues. It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.

staunton 3y ago
> hardware is a lot more likely to be mathematically proven Maybe that's a nitpick, but I would say it's fundamentally impossible to mathematically prove anything at all about a physical system. You have to assume some model to do the proof and have no way of ever "proving" (what would that even mean?) that model. I guess you're referring to the fact that verification and formal methods are used in hardware more often than software. This is due to commercial reasons: you can't just reprogram a million chips once they leave your fab.
Tainnor 3y ago
We run proofs on code all the time, it's called type-checking. What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.
kaba0 3y ago
> However the theory itself allows that all code could be mathematically proven I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.
- bluGill 3y ago
  But we never need to prove the general case, only specific cases. The general case includes an infinite number of inputs, but in reality there is only a finite number of states a physical computer can have (the number of states far exceeds the number of atoms in the universe, but it is still finite)
  - alpaca128 3y ago
    I don't think a theoretical computer scientist would agree.
    - bluGill 3y ago
      So long as the number of states is finite theory says we can prove by exhaustion. Either a state terminates, or it becomes a different state. Then you do a tree seach until you have reached a termination or a state already in the tree. You need more memory than the number of states to do this, but theroy allows for infine memory in the proof.
      - bluGill 3y ago
        Remember the halting problem is proving within a system, we can often step outside the system to prove it. Which sometimes allowes for more properties to be proved'
        drdeca 3y ago
        The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.) Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.

aeneasmackenzie 3y ago

Typical proofs don’t cover side channels, just ISA semantics. With the big asterisk that most programs are running on top of an unverified kernel on an unverified machine-level blob on an unverified ISA implemented by an unverified chip, you can absolutely prove the behavior of programs. Lamport has an unusual attitude towards verification and comes towards it from a slightly different angle, and model checking is not a good approach to machine-level proofs.

staunton 3y ago

What does it mean to say "a program is provable"? You have to prove something about it. In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.

miloignis 3y ago

If I understand what you are asking about correctly, then I do think you are mistaken. As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done. This ranges from things like CakeML (https://cakeml.org/ https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages. Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.

mapM 3y ago

I think you misunderstand. On your point about programs not being "provable": it is certainly possible to prove some properties about some programs. It is not necessarily easy, and it very much depends on the program and the property in question, but it is possible. However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.

nyrikki 3y ago
Entscheidungsproblem, the Halting problem, the total function problem, etc... typically relate to arbitrary programs. The point being is there is no single general algorithm that can solve them. The example you gave above is propositional logic, or zeroith order logic which is known to be decidable. First order logic and higher order logic are not decidable. Total functions are also not subject to the halting problem, but unfortunately finding a total function in the general case is also undecidable.
- deterministic 3y ago
  It doesn’t matter. What matters is if you can prove things you care about true for code you care about. And yes we can prove termination and zero bugs for a lot of practical useful code. Examples: seL4 is a proven correct micro kernel and CompCert is a proven correct C compiler. The trick is to use programming languages that are total i.e. not general infinite tape turing machines.

nyrikki 3y ago

Note this quote from the article. "One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox." This is similar to constraints of making something semi-decidable or recursively enumerable. Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways. Some things are easier to find in type theory, other in set theory and for some Turing machines work better. The Church–Turing thesis isn't provable but is the safe assumption. IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory. As an example related to term rewriting which will be important to ML. https://arxiv.org/abs/2307.14805 https://arxiv.org/abs/2307.14805