I haven't written a lot of decentralised code in production, but I get the impression there is generally more to consider, and a fun new class of failure modes to worry about.
Contracts are not code.
It's a complete misunderstanding to posit them as such.
Contracts depend first and foremost upon the legal regime in which they are valid. Every jurisdiction has rules, precedence, language means specific things.
There is quite a bit of variability in this stuff, which is why we have lawyers. And Judges.
Putting a contract into a crypto ... is basically pointless.
There's possibly more transparency, akin to publishing contracts on the web or something like that.
And of course, there is a 'narrow range of agreement possibilities' that could take place on crypto contracts, for example, things like stock options etc..
But generally speaking, even the contract cryptos are 'technologies looking for application'.
We don't want to 'nay say' new, dreamy ideas, but these new dreamy ideas, combined with a bit of hubris, arrogance, greed, lack of self awareness can create problems.
One could counter that no code ever stands alone, but is executed in terms of some runtime.
But I think I can bolster your point with two further thoughts:
1. Contracts are not meant to be code. The process of drafting a contract helps people arrive at a common understanding - a shared consensus, a "meeting of the minds" - and once signed, it then documents that understanding along with relevant context sufficient for third parties to be able to recreate that common understanding.
The contract is not executable - it, at best, is a declarative description of some of the outcomes. The actual execution is handled independently by the parties that entered the contract. The contract only exists so that common understanding can be preserved through time and shared with other people - whether it's because some party forgot the details, or it needs to be modified, or third parties (like lawyers, judges or arbitrators) need to be involved in dispute resolution.
2. To the extent a contract contains anything resembling executable code - say, the aforementioned declarative descriptions of outcomes, or imperative descriptions of specific behavior, or some attachments with deliverable specifications, etc. - these are all expressed in a very high-level programming language, i.e. natural language. This "code" is ultimately "executed" by sapient human beings. In other words, the programming language and runtime in questions are GAI-complete: that is, coding them up from scratch, e.g. to enable "smart" contracts to be comparable in utility to regular ones, would be equivalent to creating a human-level general-purpose artificial intelligence. We're not anywhere close to achieve that, thus by definition, "smart" contracts are too dumb to make sense when we can use the normal ones.
I think we really need to be splitting up code for smart contracts into 3 classes:
- Low Complexity, Automated Assurance: Non-turing complete DSLs that allow you to fully reason about their behaviour and catch bugs in a near completely automated manner. The only one of these that I know of at the moment is Marlowe however I'd love to know if more existed. This class should be easily accessible by finance people and should be near impossible to get wrong.
- Medium Complexity, Semi-automated Assurance: These are tools that are expressive and more code than contract however they may or may not be turing complete. These can catch a wide number of bug classes but may need manual intervention (annotations or proofs) to cover the last mile.
- High Complexity, Manual Assurance: The are tools that give you the full power of a turing complete language and all the landmines that come with them. I personally believe any smart contract written with one of these tools should not be used in production unless it is accompanied with a formal specification and an end to end set of proofs verifying correctness.
At least with this model you can judge the risk factor by how complex your application is. 90% of smart contracts probably fall into the first class and another 9% probably fall into the second. There really is no reason to be using a tool without any reasonable amount of assurances provided unless your project is extraordinarily complex (and even then it'd probably cost a fortune to run on a network) and even then there's no reason for these smart contracts to exist without any proofs backing them.
https://archetype-lang.org/ is a non-turing complete dsl that you can run http://why3.lri.fr/ proofs on.
Another way is to run proofs on the michelson that was generated by a higher level language (https://ligolang.org/, https://hackage.haskell.org/package/morley ...) with: https://gitlab.com/nomadic-labs/mi-cho-coq
The most interesting project (still alpha i think) to me is: https://juvix.org/ a rather elegant dependently typed language.
By the way what's your thought on Plutus (https://developers.cardano.org/en/programming-languages/plut...)?
It's technically its own language however it is basically a Haskell DSL/library that lifts code into a smart contract domain. It seems to retain the full expressivity and safety of Haskell (and the Haskell tooling). Additionally it allows you to share the same code base for on and off network code (as the smart contract code is largely just code lifted into a smart contract domain. This provides pretty much seamless interaction between the two domains. The documentation is a bit sparse at the moment which is its biggest weakness however that's rapidly being improved with the approach of Alonzo at the end of July/start of August.
I'm honestly so glad we as a space are finally starting to move away from Solidity and all of its footguns.
Thankfully, other cryptos (such as Cardano) are building their smart contract platform with correctness/security in mind (compiler checks and so on), so we might see less problems like this.
And stuff like "I lost £95,000 in a bank scam after my solicitor's email was hacked".[1] She managed to recover £57k after , but still lost £35k, not an insubstantial amount!
If anything, we need more protection against stuff like this. Sending money to the wrong account because your solicitor's email account was compromised is something that can happen to anyone, especially if it's someone you've been in regular contact with.
It seems the systems for dealing with fraud in the current banking system is already inadequate (although there is now a new "voluntary code" according to the article, no idea how well this works in practice), and for crypto it's woefully so.
[1]: https://www.theguardian.com/money/2020/feb/29/bank-scam-soli...
My understanding was that change basically closes the majority of these scams (where the account details are substituted) as you would now need to create an account with a name you don't have ID for which is very very hard.
As for how this actually pans out in practice: I don't know. I'd guess that having people also fill in a name isn't impossible either, although it certainly makes it a lot harder.
If I call my bank, they can fix a mistake, no matter how bad, because they own "truth".
I think what will end up happing is every contract will have the ability for some authorized key to make arbitrary movements of tokens amongst custodial accounts and nobody will build contracts where anything is moved out of custodial accounts until there's been multiple authorizations. Sort of how I transfer money into Gemini, I don't just trade from my personal checking account and they won't transfer to my checking without some authorizations. Look, I know I'm not being sophisticated here, I'm just saying, you need a way of un-fucking a fuckup and if someone can abscond with tokens easily because of a small logic flaw that doesn't work writ large.
It's just regular finance with extra steps.
The problem with loans generally isn't that you can have one at 10Am on a Sunday morning.
Try to figure out WHY things are the way they are and run through some scenarios. It's not a bullet proof system, I don't always do it well... but it can help having to re-invent some of the more obvious aspects of the wheel.
The whole blockchain ecosystem seems like a long drawn out lesson as to why at least some systems we have are kinda big, bulky, involve a lot of checking / overhead ... and why some rules and regulations exist.
Every new blockchain company that posts a blog and complains about "Why can't we just..." often has me thinking "Well yeah you shouldn't... wtf"
I hadn't read this before, but it is worded way better than I did.
As a developer I often stumble across code and systems that are superficially idiotic. I just think "Why isn't this doing X instead?".
Here there are two approaches 1) blindly change the thing to make it better 2) Try to understand why it is wrong, and what led to the legacy design.
The sensible thing might be 2, but its also soul-crushingly boring. So I obviously always do 1. After ripping out some code and replacing it with shiny new code, you invariably find the edge cases that led to the legacy design.
They will show up as bugs, or edge cases missing. After a while, you will have iterated so that your solution might look something like the original (hopefully slightly better) but the important thing is you now have a system you understand fundamentally. You basically traded a few regressions for fundamental understanding of a system
The smart contract in my hypothetical scenario might be something like a transaction with 3 parties: you (the customer), the construction company, and a third-party verification service, that executes your payment to the construction company when any 2 of the parties agree to execute. This theoretically prevents the possibility of any 1 party defecting and running away with a monetary benefit (including the third party verification service, which couldn’t run away with the cash like a traditional escrow service hypothetically could).
But my point is that even in this case, if the construction company and third-party verification service colluded to run away with the money without completing the work, you would still sue one or both of them, and my prediction is that the courts would treat this essentially identically to a scenario using traditional contracts.
If we describe these code-as-law thingys as 'dumb contracts' it is crystal clear that 'YES' this is a dumb contract and any sane judge presented with one may well decide to give the participants exactly what they deserve, just like paper-based 'dumb contracts.'
The key innovation here is that we've gone to the remedy residing in programmer malpractice, rather than attorney malpractice. Which in turn, when it becomes obvious to all involved, hopefully will have a chilling effect on any smart programmer asked to write a 'dumb contract.'
I've seen/read somewhere that Vitalik regrets naming them "smart contracts" though.
An agreement is an agreement subject to laws and jurisdiction. There's no avoiding that.
It will be interesting to see how this plays out in the courts.
If someone buys product x from seller y, which is based on some decentralized ‘contract’ which is defacto enforced by every node of the network independently - and that product then produces a unjust outcome.
You go to court, but what if Y is just a node on the network? And everyone involved is outside the courts jurisdiction? what can an adverse court judgement actually accomplish? It can’t roll back the network activity to fix the smart contract without everyone’s consent - and that seems unlikely. It can declare product X illegal or fine seller Y - but if they have no way to enforce it, what’s the point?
If Y can’t be hauled into court because they are in another country or you just don’t know their identity, well that isn’t a problem specific to these “distributed smart contracts.”
In this case, you send some ether somewhere.
Those things are not a small deal.
If the seller is unidentified, then it is possible to get a judgement and work on identifying them. If it's not just a civil dispute but felony fraud, then law enforcement might identify them some years later, it happens.
Of course, if everyone involved is properly anonymous then it's very, very hard to enforce anything, and takes enough effort and money so that it's not worth the hassle for small amounts, so for that there's simply some 'caveat emptor' in dealing with foreign anonymnous sellers. If you defraud $10 off of someone across the ocean, you are likely to get away with this. But for large cases of fraud? Everyone makes mistakes now and them that may allow them to get identified, and such fraud can be prosecuted many years later.
You could argue there will be lowered costs in the happy path where nothing goes wrong, but I'm not sure that's valid since the underlying software still needs to written/supported by someone.
This allows for a lot more efficiency as people who've never met can make trades on an open market without having to involve anyone else.
Matt Levine wrote about exactly this in a recent Money Stuff column: https://www.bloomberg.com/news/newsletters/2021-05-11/money-... . First paragraph:
> A model that I often use for cryptocurrency is that it is rediscovering traditional finance: In its early days, crypto was a brand-new financial system, unsullied by the old evils of central banking, leverage, regulation, etc.; eventually people realized that some of those things were good, and started reinventing them. One way to reinvent finance is for idealistic crypto technologists to invent banking, leverage, regulation, etc., from first principles, with cursory or no knowledge of how the traditional financial system addressed these issues or why it rejected other solutions. You would expect this to lead to flawed but interesting results, whole new ways of doing things that might blow up horribly but that might instead point the way to a better future.
As he says, "You would expect this to lead to flawed but interesting results, whole new ways of doing things that might blow up horribly but that might instead point the way to a better future".
Yeah, but shouldn't it be possible that these things will be avoided by confirming the validity of the code with theorem provers such as Coq, Lean, or something similar, at some point in the not too distant future? That's what I've been wondering, without currently having any stakes in the game (and probably not until there's compelling mathematical proof of security)
Proofs and theorems can have bugs.
I remember that in my computability theory class, defining the right proof was by far the most difficult task. And this was in very small, closed systems.
That is of course correct. However, it was my impression that the contract mentioned in the OP was completely on the blockchain, and therefore completely deterministic (no oracles or whatever.) Hence I figured it could've been proved with absolute rigor, in which case it should've been possible to formally prove the correctness. I'll be honest, I didn't look through the contract in detail now, so I might be wrong.
It doesn't change the fact that the crypto system lives in a human world were law, politics and attacks can coerce you to do a lot of things and the formality of the system is just irrelevant.
But a proof/formal methods can't actually prevent you from being wrong because you can be wrong at any meta level.
Oh, this is a definition of "correct", it's not me correcting the OP.
All the while traditional "non-distributed" finance simply uses sound engineering practices, such as code reviews, audits and sign-offs at much smaller cost and without requiring specialized PhDs in multiple unrelated fields.
Without being able to provide any evidence, I'm quite sure (that is, I hypothesize) that if a theorem is clearly stated, such as in the case of formal proof assistants, we'll soon reach a point where we'll have a distributed network in which people are able to 1) provide economic incentive for somebody to provide a given proof, 2) somebody else to potentially offer a better proof which will computationally be accepted (verified by some algorithm that prefers one proof over another by some sort of metric), and therefore 3) have a system in which the validity of a computer algorithm, which has been stated as a conjecture, can be mathematically created and verified in a decentralized fashion.
>it would need to be done by someone who actually understands both the theory of proving algorithm corectness and the algo in question
If the theorem is stated clearly, no further understanding is needed. But of course they'd need the understanding of providing the right axioms and definitions, which are as limited as possible, to state their conjecture. That, I think, will be the point at which the purpose of the mathematician will shift from providing proofs, towards discovering interesting and coherent conjectures, as the proving of those will turn into a kind of rat-race, and ultimately merely a computational challenge.
Anyways, I'm just rambling about some things that have been on my mind recently. Don't take me too seriously.
It would be better to build in a margin of tolerance for correcting mistakes, but that's contrary to the rigid determinism that smart contracts and cryptocurrencies, for some reason, strive for.
I started to have this feel already. DeFi projects creates projects that create projects .. it's gonna be a potential spaghetti bowl of intermediate layers. Either the mass is gonna make it survive on the side or it's gonna fade off xml style.
There's a reason we don't have lawyers review every ecommerce or in-store purchase that's made: the process of shopping has been standardized to such an extent that most parties (merchants and buyers) don't need to sign a bespoke agreement for every transaction.
If we can get more complex agreements automatically hammered out, it represents not just large cost savings, but potentially creating more business for smaller players easily.
c.f. people checking t&c's becuase they can't be bothered to read them (/sympathetic).
The advantage then is that you get to choose how much control you want to give up for safety. Unlike the current system where you have to use these institutions to participate.