3 ms·

If there's every a use for provably correct programs, it should be in crypto.

• nl 4y ago
  Hey Matt! There is some interesting work done in this area. For example https://reach.sh/ https://reach.sh/ lets you write formally verified smart contracts. I guess this is helpful with some classes of bugs. But I'm not sure it would with most. For example it is unclear if it would have caught this problem since (from the vague description!) it appears it would have needed some economic modelling to catch.
• RHSeeger 4y ago
  From what I'm seeing here, all the individual things that were done _were_ correct. It just so happens that the system was setup with rules that allow for this type of thing. A probably correct program would not have helped here.
  • dfcowell 4y ago
    This is the difference between correctness and fitness for purpose.
• threeseed 4y ago
  The problem is that you can't predict ahead of time every use case. That's why today's financial system has the ability to manually revert back to a previous state if something gets wrong e.g. undo transactions, government bailouts etc.