7 ms·

> but your final paragraph seems to imply the formalism isn't key to end quality? That's not what I said. I said that merely creating a verified formal specifi

by pron 7y ago

> but your final paragraph seems to imply the formalism isn't key to end quality? That's not what I said. I said that merely creating a verified formal specification of a language is not in itself a good path to increasing correctness, and I wouldn't focus on that as a significant cause for concern given all others. But even when you use formal methods in the development of your software -- and I'm certainly a proponent -- there are many formal methods with widely different guarantees and costs, and some of them don't require a formal specification of the programming language. Moreover, no system can be 100% error free, regardless of verification method used. Systems rely on hardware whose actual behavior can never be "proven" correct, and, at best, only probabilistically matches the spec. I personally believe that some formal methods can greatly improve correctness, and do so affordably, but the question of which formal methods are worthwhile when and by how much each of them improves correctness is very much an open question. > it's the only working implementation of the concept of perfectly secured data. I strongly disagree. There is no such thing as "perfectly secure." Security is defined with respect to certain threats (e.g. a hazmat suit can protect you from poisonous gas but gives you no defense from bullets, whereas a bullet-proof vest is the opposite), and blockchain is rarely the most secure with respect to the most relevant threats in a monetary system.

AlphaWeaver 7y ago
> Security is defined with respect to certain threats, and blockchain is rarely the most secure with respect to the threats in a monetary system. Wow, this is a great way to frame this! What do you see as the largest threats to the effective operation of a monetary system?
- pron 7y ago
  I think this question is best answered by economists, and I'm certainly not one. But blockchain does seem to interfere with some of the best regulatory defenses against economic disasters.
  - rossdavidh 7y ago
    Blockchain gives the impression that the primary threat it is designed to defend against, is a government deciding (like Germany between world wars) to inflate their currency for whatever reason. So, not surprisingly, in order to defend a currency against being decreased in value by a central authority, it is vulnerable to all of the threats that a central monetary authority might help you with. Which of these threats you think is the more salient is, of course, a matter on which people may disagree. I personally find the risk of a central monetary authority devaluing my money, to be not one of my top concerns, but I could understand why others might think differently (especially if they were in a different country, that used a different currency).
    - kragen 7y ago
      Right, here in Argentina our currency has lost more than half its value this year, and the US dollar has lost 96% of its value since the end of the gold standard in 1973. I carry a Zimbabwe 100 trillion dollar bill in my wallet to remind people what real hyperinflation is. I don't think that's the main threat Bitcoin is designed to defend against, though; I think there's a whole spectrum of confiscation threats, ranging from thieves tunneling into bank vaults (I know a woman here who lost her savings that way), to immigration authorities confiscating jewelry, to pirates, to trumped-up "money laundering" charges. And of course if we're mentioning Germany and World Wars, we must not forget the confiscation of Holocaust victims' entire possessions, including jewelry and fillings after the gas chambers. Bitcoin can't make genocide impossible but maybe at least it can make it unprofitable.
      - rossdavidh 7y ago
        I see your point, but I think there are plenty of examples of people losing their Bitcoins through analogous nefarious activities (e.g. MtGox). For an expert in cybersecurity perhaps Bitcoin is safer, but for the average non-technical person (in the U.S.) it is probably _more_ likely to get your money taken by a thief than if you had it in fiat currency in a bank, though of course either one is possible. Again, this could vary depending upon your nation's government and crime situation.
- pyrale 7y ago
  Basically, scams. The ability to block a planned payment or ask your bank to chargeback is one of the keys to trust in online economy. If our banking system had used something like bitcoin to implement online transactions, odds are that e-business would have had much less successs and much higher barrier to entry.
  - nybble41 7y ago
    Given a system with irreversible transactions you can always add structure on top to support escrow, chargebacks, or whatever other protection mechanisms you deem prudent. It doesn't work so well the other way around.
    - PeterisP 7y ago
      Protection from scams requires that a malicious actor with full technical control of some account is still unable to make irreversible transactions by opting out of whatever structure supports escrow, chargebacks, etc; so either those mechanisms (conditional reversibility, with technical controls defining a reasonable regime of when reversals will be possible and when not) are built in the core system and aren't optional, or the system doesn't have a sufficiently usable reversibility because all the really large scams will simply avoid that "structure on top". The other alternative, of course, is someone taking on full legal liability for transactions that can't be secured technically. If Facebook would offer Libra to consumers in e.g. UK, then all that "transactions are technically irreversible" means is that Facebook would be required to "reverse" the transaction to customer while being unable to recover the funds from the beneficiary - and if they can afford to do that, that's their choice to make.
      - nybble41 7y ago
        You're asking way too much. It's not as if the current system actively prevents you from opting out of all the safety measures and, say, irreversibly handing cash (or something else of value) directly to a scammer; nor should it. Reversible transactions come with costs, especially when the other side of the transaction is not reversible. Chargeback fraud, for example, is a big problem for merchants, and can only occur in a system with reversible transactions. Contracting parties should be free to negotiate both the form of payment and the degree of risk each side is willing to take. The main problem is simply the novelty of it all. Once reasonable and customary structures to handle disputes are in common use asking people to bypass those structures without a very good reason will be just as much of a red flag as it is under the current system. Facebook is not a party to a transaction between any other two Libra users and should have no liability in the event of a dispute over payments beyond maintaining accurate records and providing a fair and above all neutral platform to conduct business.
- jpadkins 7y ago
  There are a lot of minor threats to monetary systems that blockchain does not address. Bitcoin addresses the rare but fatal threat of hyperinflation (runaway inflation). Historical examples https://en.wikipedia.org/wiki/Hyperinflation#Notable_hyperinflationary_episodes https://en.wikipedia.org/wiki/Hyperinflation#Notable_hyperin... The only known solution to this threat is not have a single supplier of money (i.e. a lot of independent miners digging metal out of the ground, or the block chain equivalent)
K0SM0S 7y ago
Exactly what I needed to hear, thanks again. I reckon the only way to error-free is redundancy, i.e. 'out of the box' we just put two boxes, or actually three for "high availability"; the underlying controller being just a dead man's switch — if A's life signal dies, failover to B; set up C as new failover; reboot A. > I personally believe that some formal methods can greatly improve correctness, and do so affordably, but the question of which formal methods are worthwhile when and by how much each of them improves correctness is very much an open question. Oh I can see that. In general terms, I think cost should be focused on the most critical components; like we don't need to test every single bit of code before production. You just crash gracefully and resume state when the loss (if any) is acceptable. When it's not, then it's not a choice to front the cost, it's an imperative, part of your 'spec' as a business/product/service/free thing. Tor is slower than normal browsing, but that's the tradeoff. Fast forward 10 years and costly workloads have become either accelerated by hardware or simply benefit from general improvements, like encryption is now fundamentally cost-free for usual things like TLS (AES-based things), or increasingly AI workloads. > blockchain is rarely the most secure with respect to the most relevant threats in a monetary system. I very much agree. Key words being "in a monetary system", and indeed it's about economics more than tech (what I alluded to in saying 'Earth circa 2019', i.e. globalized monetary system, central-bank driven, mostly insured for most customers, etc). Hence why I advocate that blockchain proponents explore other domains. I know businesses are, but it has more to do with topics like compliance (internal, legal).
- pjc50 7y ago
  > I reckon the only way to error-free is redundancy, i.e. 'out of the box' we just put two boxes, or actually three for "high availability"; the underlying controller being just a dead man's switch — if A's life signal dies, failover to B; set up C as new failover; reboot A. You can have a lot of this automatically with "lockstep" chips, such as TI Hercules: http://www.ti.com/en/download/mcu/SPRB204.pdf?DCMP=hercules&HQS=hercules-mc http://www.ti.com/en/download/mcu/SPRB204.pdf?DCMP=hercules&...
  - K0SM0S 7y ago
    Very interesting! Duly noted, thanks for the pointer.
michaelmrose 7y ago
>That's not what I said. I said that merely creating a verified formal specification of a language is not in itself a good path to increasing correctness, and I wouldn't focus on that as a significant cause for concern given all others. This seems to be poorly considered. Isn't it easier for an OS and a language to be verified once even at great cost than hoping future billions of lines of developer code already produced at lesser cost per line are actually correct? https://microkerneldude.wordpress.com/2016/06/16/verified-software-can-and-will-be-cheaper-than-buggy-stuff/ https://microkerneldude.wordpress.com/2016/06/16/verified-so...
- pron 7y ago
  A formal specification for the programming language doesn't automatically verify all programs written in it; in fact it verifies none, or at most one. It serves two purposes: it defines what each language primitive does so that proofs of programs written in the lang can make use of those definitions, and sometimes it is also used to verify that a compiler indeed preserves the language's semantics, as defined in the spec, when translating it to some other language; in other words, it can be used to verify the compiler. Focusing on a formal language spec is like saying that a good way to make your software more correct is to work hard to ensure your compiler doesn't have bugs. I'm sure you'll agree there are more important things. As to use by program proofs, often an approximate ad-hoc specification is good enough. BTW, the article you linked to is about one particular formal method -- deductive proof. There are many others, with varying costs and benefits.

by pron 7y ago

AlphaWeaver 7y ago

> Security is defined with respect to certain threats, and blockchain is rarely the most secure with respect to the threats in a monetary system. Wow, this is a great way to frame this! What do you see as the largest threats to the effective operation of a monetary system?

pron 7y ago
I think this question is best answered by economists, and I'm certainly not one. But blockchain does seem to interfere with some of the best regulatory defenses against economic disasters.
- rossdavidh 7y ago
  Blockchain gives the impression that the primary threat it is designed to defend against, is a government deciding (like Germany between world wars) to inflate their currency for whatever reason. So, not surprisingly, in order to defend a currency against being decreased in value by a central authority, it is vulnerable to all of the threats that a central monetary authority might help you with. Which of these threats you think is the more salient is, of course, a matter on which people may disagree. I personally find the risk of a central monetary authority devaluing my money, to be not one of my top concerns, but I could understand why others might think differently (especially if they were in a different country, that used a different currency).
  - kragen 7y ago
    Right, here in Argentina our currency has lost more than half its value this year, and the US dollar has lost 96% of its value since the end of the gold standard in 1973. I carry a Zimbabwe 100 trillion dollar bill in my wallet to remind people what real hyperinflation is. I don't think that's the main threat Bitcoin is designed to defend against, though; I think there's a whole spectrum of confiscation threats, ranging from thieves tunneling into bank vaults (I know a woman here who lost her savings that way), to immigration authorities confiscating jewelry, to pirates, to trumped-up "money laundering" charges. And of course if we're mentioning Germany and World Wars, we must not forget the confiscation of Holocaust victims' entire possessions, including jewelry and fillings after the gas chambers. Bitcoin can't make genocide impossible but maybe at least it can make it unprofitable.
    - rossdavidh 7y ago
      I see your point, but I think there are plenty of examples of people losing their Bitcoins through analogous nefarious activities (e.g. MtGox). For an expert in cybersecurity perhaps Bitcoin is safer, but for the average non-technical person (in the U.S.) it is probably _more_ likely to get your money taken by a thief than if you had it in fiat currency in a bank, though of course either one is possible. Again, this could vary depending upon your nation's government and crime situation.
pyrale 7y ago
Basically, scams. The ability to block a planned payment or ask your bank to chargeback is one of the keys to trust in online economy. If our banking system had used something like bitcoin to implement online transactions, odds are that e-business would have had much less successs and much higher barrier to entry.
- nybble41 7y ago
  Given a system with irreversible transactions you can always add structure on top to support escrow, chargebacks, or whatever other protection mechanisms you deem prudent. It doesn't work so well the other way around.
  - PeterisP 7y ago
    Protection from scams requires that a malicious actor with full technical control of some account is still unable to make irreversible transactions by opting out of whatever structure supports escrow, chargebacks, etc; so either those mechanisms (conditional reversibility, with technical controls defining a reasonable regime of when reversals will be possible and when not) are built in the core system and aren't optional, or the system doesn't have a sufficiently usable reversibility because all the really large scams will simply avoid that "structure on top". The other alternative, of course, is someone taking on full legal liability for transactions that can't be secured technically. If Facebook would offer Libra to consumers in e.g. UK, then all that "transactions are technically irreversible" means is that Facebook would be required to "reverse" the transaction to customer while being unable to recover the funds from the beneficiary - and if they can afford to do that, that's their choice to make.
    - nybble41 7y ago
      You're asking way too much. It's not as if the current system actively prevents you from opting out of all the safety measures and, say, irreversibly handing cash (or something else of value) directly to a scammer; nor should it. Reversible transactions come with costs, especially when the other side of the transaction is not reversible. Chargeback fraud, for example, is a big problem for merchants, and can only occur in a system with reversible transactions. Contracting parties should be free to negotiate both the form of payment and the degree of risk each side is willing to take. The main problem is simply the novelty of it all. Once reasonable and customary structures to handle disputes are in common use asking people to bypass those structures without a very good reason will be just as much of a red flag as it is under the current system. Facebook is not a party to a transaction between any other two Libra users and should have no liability in the event of a dispute over payments beyond maintaining accurate records and providing a fair and above all neutral platform to conduct business.
jpadkins 7y ago
There are a lot of minor threats to monetary systems that blockchain does not address. Bitcoin addresses the rare but fatal threat of hyperinflation (runaway inflation). Historical examples https://en.wikipedia.org/wiki/Hyperinflation#Notable_hyperinflationary_episodes https://en.wikipedia.org/wiki/Hyperinflation#Notable_hyperin... The only known solution to this threat is not have a single supplier of money (i.e. a lot of independent miners digging metal out of the ground, or the block chain equivalent)

K0SM0S 7y ago

Exactly what I needed to hear, thanks again. I reckon the only way to error-free is redundancy, i.e. 'out of the box' we just put two boxes, or actually three for "high availability"; the underlying controller being just a dead man's switch — if A's life signal dies, failover to B; set up C as new failover; reboot A. > I personally believe that some formal methods can greatly improve correctness, and do so affordably, but the question of which formal methods are worthwhile when and by how much each of them improves correctness is very much an open question. Oh I can see that. In general terms, I think cost should be focused on the most critical components; like we don't need to test every single bit of code before production. You just crash gracefully and resume state when the loss (if any) is acceptable. When it's not, then it's not a choice to front the cost, it's an imperative, part of your 'spec' as a business/product/service/free thing. Tor is slower than normal browsing, but that's the tradeoff. Fast forward 10 years and costly workloads have become either accelerated by hardware or simply benefit from general improvements, like encryption is now fundamentally cost-free for usual things like TLS (AES-based things), or increasingly AI workloads. > blockchain is rarely the most secure with respect to the most relevant threats in a monetary system. I very much agree. Key words being "in a monetary system", and indeed it's about economics more than tech (what I alluded to in saying 'Earth circa 2019', i.e. globalized monetary system, central-bank driven, mostly insured for most customers, etc). Hence why I advocate that blockchain proponents explore other domains. I know businesses are, but it has more to do with topics like compliance (internal, legal).

pjc50 7y ago
> I reckon the only way to error-free is redundancy, i.e. 'out of the box' we just put two boxes, or actually three for "high availability"; the underlying controller being just a dead man's switch — if A's life signal dies, failover to B; set up C as new failover; reboot A. You can have a lot of this automatically with "lockstep" chips, such as TI Hercules: http://www.ti.com/en/download/mcu/SPRB204.pdf?DCMP=hercules&HQS=hercules-mc http://www.ti.com/en/download/mcu/SPRB204.pdf?DCMP=hercules&...
- K0SM0S 7y ago
  Very interesting! Duly noted, thanks for the pointer.

michaelmrose 7y ago

>That's not what I said. I said that merely creating a verified formal specification of a language is not in itself a good path to increasing correctness, and I wouldn't focus on that as a significant cause for concern given all others. This seems to be poorly considered. Isn't it easier for an OS and a language to be verified once even at great cost than hoping future billions of lines of developer code already produced at lesser cost per line are actually correct? https://microkerneldude.wordpress.com/2016/06/16/verified-software-can-and-will-be-cheaper-than-buggy-stuff/ https://microkerneldude.wordpress.com/2016/06/16/verified-so...

pron 7y ago
A formal specification for the programming language doesn't automatically verify all programs written in it; in fact it verifies none, or at most one. It serves two purposes: it defines what each language primitive does so that proofs of programs written in the lang can make use of those definitions, and sometimes it is also used to verify that a compiler indeed preserves the language's semantics, as defined in the spec, when translating it to some other language; in other words, it can be used to verify the compiler. Focusing on a formal language spec is like saying that a good way to make your software more correct is to work hard to ensure your compiler doesn't have bugs. I'm sure you'll agree there are more important things. As to use by program proofs, often an approximate ad-hoc specification is good enough. BTW, the article you linked to is about one particular formal method -- deductive proof. There are many others, with varying costs and benefits.