Technology and how it evolves

Hi Cardano Forum
As Cardano moves onwards and upwards, i’m interested to learn how the tech compares to other blockchains and to better understand how Cardano may be/is better.
I read this article some time ago and would appreciate someone with greater knowledge/skills than myself to offer their view of Cardano v ETH, also do you know if ETH2 resolves the challenges highlighted in this article and how ETH2 actually addresses those shortcomings of ETH.

Thanks

1 Like

I don’t know much about Eth2, but after learning about the Cardano approach with Haskell, Formal Methods, and formal verification, combined with extensive peer review, I find it hard to trust that anything built to lesser standards will still be around in 5 or 10 years. What assurances do investors/stakeholders have that Eth2 won’t introduce some critical flaw that brings down the whole system? It’ll probably work great for a while, until one day it that doesn’t.

1 Like

Formal verification does allow producing bug-free code, but only with the understanding that a bug-free software is one that strictly adheres to its specification. For the sake of illustration, let’s imagine the navigation software (the one that computes thrust) of a rocket is formally verified, then you upgrade the engine without updating the specs and the code to reflect the change of input parameters domain, your rocket will eventually go boom, even though the software was not inherently flawed. So it’s a necessary but not sufficient condition toward this goal.

Formal verification of source code is definitely a great advance however computers don’t feed of source code but of machine code, the step that converts source code to machine code (well, assembly code then machine code) is done by a compiler (and an assembler). There are indeed formally verified compilers, e.g. CompCert for the C language but apparently there isn’t one for Haskell that I know of, yet. Not short of looking for it.

Concerning the DAO hack, I believe it was more a smart-contract error than an Ethereum conception error, there have been other cases since, sometimes even with previously audited code. After all, smart contracts are programs and as such they could be independently formally verified.

«They must consider that great responsibility follows inseparably from great power.»

Unknown author (French National Convention, 1793)

1 Like