Comment by seanhunter
5 years ago
>> Judging by how most people write code today, I find this idea terrifying
> Most people today don't write code for safety critical systems. The abstract mentions they already uncovered a "bug" in an active law by rewriting it in their language, so it could be an immensely helpful tool for finding edge cases and loopholes in that mess.
I'll give you an example from a field that I (unfortunately) have a reasonable amount of experience of where the law and contracts are supposed to be interpreted 100% literally like an algorithm: structured finance (eg the subject matter of the 2008 financial crisis). The prospectus of a structured security like a mortgage bond is typically a hundred or more pages of very dense legalese that was worked on intensively by highly-specialised lawyers and bankers for months. Its intent is to set up a small special-purpose company with strict rules on how it operates down to the last penny and zero discretion. This allows investors (in theory) to understand how the bond will perform.
The opening chapter of my introductory textbook on structured credit analysis says the author (who has been part of those teams for years and has worked on hundreds or possibly thousands of bonds) has never read a bond prospectus for a structured security that does not contain serious drafting errors. I personally worked on a bond for months and read, edited and commented on the bond model and prospectus hundreds of times. We certainly were trying to make our prospectus as simple, clear and loophole-free as possible. Then a few years after it launched we discovered we had made a big mistake in drafting it that had gone unnoticed by me, the expert bankers and lawyers and all the investors so far. Luckily we were able to fix the problem without negative consequences. There is literally no chance that this error would have been found or solved by a formal system and if anything it would actually have been worse.
Some things are complex enough that they are just very hard to do. The existing system allows for that by having a rigorous process of dispute, interpretation and argument to decide complex questions post facto.
> we discovered we had made a big mistake in drafting it that had gone unnoticed by me, the expert bankers and lawyers and all the investors so far. There is literally no chance that this error would have been found or solved by a formal system and if anything it would actually have been worse.
There is no chance that a formal system wouldn't have revealed this bug? Static analysis and simulations wouldn't have helped?
> Some things are complex enough that they are just very hard to do.
I agree with this wholeheartedly. Engineers have the ability to automate some very complex issues. But there will always be a class of issues beyond automation, simulation, analysis, etc. and we just have to accept that the only way to solve them is with slow, hard, error-prone work.
Do you think that smart contacts could be useful in this area?
Not smart contracts exactly but there is a specific part of each bond called the waterfall (basically specifies what happens with all the cashflows under different circumstances and is a little bit like an equity cap table plus liquidity preferences). I've always thought there should be a dsl specifying the waterfall that can be used for the bond model and used to generate the legalese in the prospectus. A common problem is the bond model doesn't match the prospectus and that problem would just disappear. I intend to do this as a research project if I ever get time (it's been 12 years since I had the idea to do this so it may never happen...).
If I understand it correctly smart contracts are just another piece of software combined with some blockchain magic. If you can't prove a piece of code is correct, wrapping it in a trendy buzzword won't make the code more correct.
Maybe I'm wrong, but I don't know how decentralization would change anything other than adding safeties against manipulation if done right.