4 ms·

> because nobody likes to lose their live savings because they missed a semicolon. Yeah, but shouldn't it be possible that these things will be avoided by conf

by sva_ 5y ago

> because nobody likes to lose their live savings because they missed a semicolon. Yeah, but shouldn't it be possible that these things will be avoided by confirming the validity of the code with theorem provers such as Coq, Lean, or something similar, at some point in the not too distant future? That's what I've been wondering, without currently having any stakes in the game (and probably not until there's compelling mathematical proof of security)

Daishiman 5y ago
Theorem provers require code for defining what you want to prove and the method through which you reach said proof. Proofs and theorems can have bugs.
- sva_ 5y ago
  But aren't proofs exact in what they state? So it wouldn't be the proof that would be faulty. It'd be the interpretation of what somebody thinks the proof means to them, and that'd be something you could entirely objectively reason/work on.
  - astrange 5y ago
    Proofs are programs and programs are proofs of themselves. The ways proofs might help you show that a program is "correct" (what you meant to say) are 1. the effect of writing it twice in different languages 2. that proofs may be more abstract and you can refine the program from them. But a proof/formal methods can't actually prevent you from being wrong because you can be wrong at any meta level.
    - astrange 5y ago
      > "correct" (what you meant to say) Oh, this is a definition of "correct", it's not me correcting the OP.
  - Daishiman 5y ago
    But the human world is not exact and full of context. Even mathematical.proofs exist within a context of an axiomatic system, known proofs, and various domain assumptions. I remember that in my computability theory class, defining the right proof was by far the most difficult task. And this was in very small, closed systems.
    - sva_ 5y ago
      > But the human world is not exact and full of context. That is of course correct. However, it was my impression that the contract mentioned in the OP was completely on the blockchain, and therefore completely deterministic (no oracles or whatever.) Hence I figured it could've been proved with absolute rigor, in which case it should've been possible to formally prove the correctness. I'll be honest, I didn't look through the contract in detail now, so I might be wrong.
      - Daishiman 5y ago
        It's possible that maybe, just maybe, the interior world of some crypto scheme may have sufficient formal proofs. It doesn't change the fact that the crypto system lives in a human world were law, politics and attacks can coerce you to do a lot of things and the formality of the system is just irrelevant.
janoc 5y ago
That would cost an arm-and-leg, it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question and systems like CoQ are from being able to prove large, complex systems. All the while traditional "non-distributed" finance simply uses sound engineering practices, such as code reviews, audits and sign-offs at much smaller cost and without requiring specialized PhDs in multiple unrelated fields.
- sva_ 5y ago
  >That would cost an arm-and-leg, Without being able to provide any evidence, I'm quite sure (that is, I hypothesize) that if a theorem is clearly stated, such as in the case of formal proof assistants, we'll soon reach a point where we'll have a distributed network in which people are able to 1) provide economic incentive for somebody to provide a given proof, 2) somebody else to potentially offer a better proof which will computationally be accepted (verified by some algorithm that prefers one proof over another by some sort of metric), and therefore 3) have a system in which the validity of a computer algorithm, which has been stated as a conjecture, can be mathematically created and verified in a decentralized fashion. >it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question If the theorem is stated clearly, no further understanding is needed. But of course they'd need the understanding of providing the right axioms and definitions, which are as limited as possible, to state their conjecture. That, I think, will be the point at which the purpose of the mathematician will shift from providing proofs, towards discovering interesting and coherent conjectures, as the proving of those will turn into a kind of rat-race, and ultimately merely a computational challenge. Anyways, I'm just rambling about some things that have been on my mind recently. Don't take me too seriously.
- DennisP 5y ago
  Smart contracts are not large, complex systems, and formal proofs have already been used for them. There's not much code to verify and bugs are very expensive, so the economics easily justify doing it.
the_local_host 5y ago
> ...shouldn't it be possible that these things will be avoided by confirming the validity of the code... It would be better to build in a margin of tolerance for correcting mistakes, but that's contrary to the rigid determinism that smart contracts and cryptocurrencies, for some reason, strive for.

by sva_ 5y ago

Daishiman 5y ago

Theorem provers require code for defining what you want to prove and the method through which you reach said proof. Proofs and theorems can have bugs.

sva_ 5y ago
But aren't proofs exact in what they state? So it wouldn't be the proof that would be faulty. It'd be the interpretation of what somebody thinks the proof means to them, and that'd be something you could entirely objectively reason/work on.
- astrange 5y ago
  Proofs are programs and programs are proofs of themselves. The ways proofs might help you show that a program is "correct" (what you meant to say) are 1. the effect of writing it twice in different languages 2. that proofs may be more abstract and you can refine the program from them. But a proof/formal methods can't actually prevent you from being wrong because you can be wrong at any meta level.
  - astrange 5y ago
    > "correct" (what you meant to say) Oh, this is a definition of "correct", it's not me correcting the OP.
- Daishiman 5y ago
  But the human world is not exact and full of context. Even mathematical.proofs exist within a context of an axiomatic system, known proofs, and various domain assumptions. I remember that in my computability theory class, defining the right proof was by far the most difficult task. And this was in very small, closed systems.
  - sva_ 5y ago
    > But the human world is not exact and full of context. That is of course correct. However, it was my impression that the contract mentioned in the OP was completely on the blockchain, and therefore completely deterministic (no oracles or whatever.) Hence I figured it could've been proved with absolute rigor, in which case it should've been possible to formally prove the correctness. I'll be honest, I didn't look through the contract in detail now, so I might be wrong.
    - Daishiman 5y ago
      It's possible that maybe, just maybe, the interior world of some crypto scheme may have sufficient formal proofs. It doesn't change the fact that the crypto system lives in a human world were law, politics and attacks can coerce you to do a lot of things and the formality of the system is just irrelevant.

janoc 5y ago

That would cost an arm-and-leg, it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question and systems like CoQ are from being able to prove large, complex systems. All the while traditional "non-distributed" finance simply uses sound engineering practices, such as code reviews, audits and sign-offs at much smaller cost and without requiring specialized PhDs in multiple unrelated fields.

sva_ 5y ago
>That would cost an arm-and-leg, Without being able to provide any evidence, I'm quite sure (that is, I hypothesize) that if a theorem is clearly stated, such as in the case of formal proof assistants, we'll soon reach a point where we'll have a distributed network in which people are able to 1) provide economic incentive for somebody to provide a given proof, 2) somebody else to potentially offer a better proof which will computationally be accepted (verified by some algorithm that prefers one proof over another by some sort of metric), and therefore 3) have a system in which the validity of a computer algorithm, which has been stated as a conjecture, can be mathematically created and verified in a decentralized fashion. >it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question If the theorem is stated clearly, no further understanding is needed. But of course they'd need the understanding of providing the right axioms and definitions, which are as limited as possible, to state their conjecture. That, I think, will be the point at which the purpose of the mathematician will shift from providing proofs, towards discovering interesting and coherent conjectures, as the proving of those will turn into a kind of rat-race, and ultimately merely a computational challenge. Anyways, I'm just rambling about some things that have been on my mind recently. Don't take me too seriously.
DennisP 5y ago
Smart contracts are not large, complex systems, and formal proofs have already been used for them. There's not much code to verify and bugs are very expensive, so the economics easily justify doing it.

the_local_host 5y ago

> ...shouldn't it be possible that these things will be avoided by confirming the validity of the code... It would be better to build in a margin of tolerance for correcting mistakes, but that's contrary to the rigid determinism that smart contracts and cryptocurrencies, for some reason, strive for.