> No, we can. We just don't, because it's very expensive, and we lack proper tooling to make it cheaper and/or faster. Eh, it depends on how amenable your stan

> No, we can. We just don't, because it's very expensive, and we lack proper tooling to make it cheaper and/or faster. Eh, it depends on how amenable your standards for correctness are to formalization. Also when it comes to security, where clearly bugs tend to hurt a lot more, we're almost always at the mercy of "unproven" (in the formal sense) algorithms. Don't get me started on quantum computing's effects. Reasoning about concurrent programs (let alone distributed ones) is something where I don't think we've got many reasonable schemes, even at the academic level. Though it's great to hear the Ethereum foundation is willing to drop some cash on that problem! I wish luck to anyone who takes them up on that, it's something I'd love to work on if I didn't have existing projects.