I agree; I've been trying to get employers/coworkers to look into TLA+ or Isabelle (for different things) for years now, and it feels like only after every cryptocurrency started blogging did they start to listen.
I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements.
NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?
This is because banks rely on property rights, which are enforced by courts, whereas cryptocurrencies operate on a "fait accompli" basis (i.e. whoever happens to control the coins, owns them). This means, in the cryptocurrency world, mistakes are irreversible. In conventional finance, this is not usually the case.
Sorry for replying to an old thread, but I wanted to respond to this.
I totally understand why blockchain isn't the standard for everything right now; my statement was in regards to formal methods to ensure correctness. For example, "reversing" a transaction could totally be modeled in TLA+ (and probably other systems, I'm just most familiar with TLA+ than most other systems), which would provide model checking (and possibly even proofs) that you would not otherwise have.
Your English is excellent - as a native speaker I wouldn’t have guessed you had a different mother tongue. ‘Fait accompli’ is used in English with the same meaning. I was trying to make a stupid joke referring to fiat currency… HN is a tough audience, and I’m more of a droll engineer type.
Yeah, which always felt like that would be a great reason to formally verify...If a race condition ends up draining my account of all my money, you can bet that I am going to sue for the lost funds and probably a bunch of other things, which I cannot imagine would be very cheap for the bank. In fact, I would think it would be expensive for them even if it wasn't their fault (e.g. maybe there was no money in my account because I just have bad spending habits and a bad memory).
It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
That is correct- there are all sorts of human and procedural buffers built into bank operations. Correctness of the system- and there is never just one system, there are at minimum dozens, even in the smallest bank- is not a hard requirement.
In fact you would immediately seek another job if you came from formal methods practice and then saw production code at just about any of the different animals called banks.
I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements.
NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?