This essay explores the emerging formalist and intuitionist programmer factions in the crypto community. Formalists view software development as software engineering and treat it as a branch of mathematics. Intuitionists view software engineering as software development and treat writing software as poet writes a work of art. I will analyze both approaches to programming and the security implications. #ethereum #tauchain #tau #crypto #programming
Formalist vs intuitionist factions in software engineering.
Currently the development of software is led primarily by the intuitionist faction. As a result the languages are expressive, code is less like mathematics, software is not formally modeled and verified before construction, and Turing complete is the norm. This contrasts with the formalist approach which views programs as proofs, which treats software development as an engineer or architect treats building an electronic device or a house, where precision as important, where software is to be correct by construction, where langsec is critical, where functional dependently typed languages are preferred.
In a recent article about Ethereum we can see clearly the flaw of the intuitionist approach to software development. Ethereum smart contracts have flaws and in an article titled “Ethereum contracts are going to be candy for hackers”. In the article it cites an important metric for tracking code which is the bugs per line of code ratio which tracks defects. Ethereum smart contracts on average contain 100 bugs per 1000 lines of code while NASA contains 0. The article highlights the fact that smart contracts which are buggy are dangerous.
Turing complete smart contracts follow the intuitionist school of programming. Generative Design Paradigm
The intuitionist school of programming is the mainstream and as a result the choice was made by the Ethereum team to go with Turing complete smart contracts. At the time and even to this day very few people have seriously considered the drawbacks of Turing complete. The risk vs benefit ratio of going with Turing complete smart contracts clearly is not in favor of it when you look at the fact that when you choose Turing complete you lose consistency, and as a result the expenses are actually increased due to the necessity of auditing code, of checking for bugs, and of course the halting problem which Ethereum dodged with gas.
Ethereum’s security is delivered through the security by isolation approach. Virtual machines, principle of least privilege, separation of powers, all are used to provide security for Ethereum. Essentially the security of Ethereum is maintained through isolation of processes but the problems still remain in that while the virtual machine may be audited by many eyes, and while the halting problem may be dodged by gas, the majority of smart contracts themselves are not being made following a correct by construction approach and any bug at all which goes undetected could result in a financial black hole for unfortunate investors.
Logically consistent formally verified smart contracts are the path of the formalist school of programming.
Formal verification process
In the formalist school of thought all programs are proofs. This is factually evident as a result of Curry–Howard isomorphism. In addition because the formalist school treats software engineering as mathematics there is a very logical approach to programming. The security of smart contracts under the formal approach is through logic itself and the fact that you have decidability. This decidability means you always get a yes or no answer and you have total logical consistency. This contrasts with the approach taken by Turing complete imperative programming languages such as Solidity which have smart contracts which can avoid infinite loops using gas but which can still have bugs, underhanded code, and behaviors which are unpredictable.
Formal smart contracts are verified as correct, are fully bug proof, are fully deterministic and predictable. Fully functional dependently typed programming languages are not as well known and for this reason many intuitionist developers may not be aware that it is possible to do write bug proof code. Tauchain is the only example of the formal approach being taken in the public blockchain space to date (perhaps because it’s developer Ohad Asor is a mathematician) and while other developers apply correct by construction approaches such as what we see with the Synereo team or with Casper, these projects still are built on top of a Turing complete foundation while the Tauchain project is building a new programming formal language called Tau from the ground up.
Formalist and intuitionist factions have to join forces and work together.
It may not be necessary or realistic to expect the developer community to choose one side or the other. Ethereum developers who choose to write serious smart contracts should consider taking the formal approach. This can be accomplished through correct by construction where their software is modeled , formally specified, using a design by contract method with software such as Perfect Developer.
Design by Contract
To write smart contracts in this way may take longer but it should become the standard way for financial smart contracts or smart contracts which may be used in elections such as in the Ukraine. If lives or life savings may be at stake then it makes sense to use correct by construction and to rely on formal specification even if you must hire a mathematician to write up a formal spec.
Reducing the attack surface is the goal and Tauchain may offer a synergy.
When we look at the security reasons to favor blockchain technology the idea is to spread the risk and minimize the attack surface. When the risk is centralized and there is a central point of failure in a system then it is very easy to topple the system. We’ve seen these central points of failure as central points of trust, and we keep seeing the same picture over and over again. Blockchains are supposed to minimize trust yet the current culture of the moment is a culture where we must trust core developers, curators, auditors. What Tau offers is a separation of duties where the trust is further minimized so that you do not have to trust the programmers.
The synergy Tau offers to Ethereum is that the critical portions of a smart contract can be written in Tau but the less critical portion can be written in Solidity. In cases where you don’t want to have to trust your programmer as an investor you can use Tau. This may be necessary because while with Ethereum there may be a shortage of developers who can write bug free code whom you can trust with your money it might be much cheaper to get bug free code on Tau.
Code or money, which comes first?Logo of Tau
On Tauchain there is to be built a market to be called Agoras. Agoras will allow for the hiring of coders who will code directly to a formal specification. If we remember that programs are proofs, and if we understand the implications of the Tau programming language, then we discover that a fully automated process can determine whether the code meets the specification precisely. As a result of this, there is no need for the community to trust the coder and the job of the coder can become similar to what you see on Amazon Turk where money is put up, a formal spec is provided, and many groups of coders can converge to generate the code.
Conclusion
The division between the formal and intuitionist school of programming began in 1960s and over time this has led to a decreasing reliability of software. At the same time society is depending on software more than ever before and at this point in time we trust our algorithms to know us better than we know ourselves. This trust in algorithms is a trust in mathematics, and it is just like building a bridge in or structure in ancient times. In ancient times when an architect built something such as a bridge it was a common practice for the architect to stand under the bridge while chariots crossed it to prove it could withstand the weight. In the era of smart contracts written by totally anonymous developers we now have no way to trust the code and this is evident from the controversy around Truecrypt, around Tor, around OpenSSL. When software must be written without trust then you gain benefit from the formal approach yet when software is written with trust then the developer who wrote it is held accountable. A formal approach reduces the risks for both developers and for the users in environments of low trust.
References
- http://vessenes.com/ethereum-contracts-are-going-to-be-candy-for-hackers/
- http://www.eschertech.com/products/correct_by_construction.php
- http://www.idni.org/blog/code-and-money
- https://ncatlab.org/nlab/show/computational+trinitarianism
- http://c2.com/cgi/wiki?CorrectByConstruction
- http://mcs.open.ac.uk/mj665/FormalismAndIntuition.pdf
As a non-programmer and non-mathematician, I've been looking into tau for a few days, trying to understand what it's all about. It's really hard with the lack of education that I have, and it seems that it is hard for programmers too.
The benefits of decidable programs just don't become obvious to a layperson like me as long as the talk is at an abstract level, even though the concept is understandable. However, after you mentioned that bugs in software like Tor and OpenSSL are because of intuitionist/turing-complete programming, my eyes started to open to the potential of the project. Thanks!
If I understand it right, it's easier to program in the intuitionist way, and practically all existing software libraries are such. Even Tau itself is being programmed in C++, which I find a little contradictory, but never mind. It seems to me that what the project is doing is starting a completely new ecosystem from a clean table, with an ever expanding library of totally new, bug-free, provable, reusable functions free for anyone to use. It will start off with practically nothing but the rules, and gradually accumulate a variety of libraries, which will make programming for Tau easier and easier. The libraries will provide perfect abstraction; you don't need to worry about the inner workings of it, because it will function consistently, and thus it will be a good platform to build upon. There is a huge uphill, where the benefits are small in the beginning, but which will become massive and obvious over time.
Aside from the long term prospect, there is an immediate benefit from combining consistent programs with a blockchain, namely the possibility to "trustlessly" and automatically validate someone else's code or the results of running a program. This supposedly makes it possible to "trustlessly" outsource both computing power and programming, which hasn't been possible before (?). This will of course open up huge possibilities, and that's where Agoras comes in. Tauchain itself doesn't have a token or a revenue-model, but Agoras does. Agoras needs Tauchain to function, so the creators are crowdfunding Agoras and using the funds to create Tauchain. It will surely take many years to start generating any profit, but the potential is apparently huge.
I think Agoras (AGRS) might be a hidden gem, an investment opportunity, because it is so hard to comprehend. Bitcoin is hard for people to understand, which made it a good opportunity for those who grasped the concept before the masses. So was Ethereum; it was hard to understand and very ambitious, but gave good returns for those who made the effort to understand. The benefits of Tauchain aren't obvious at all, and require quite some thinking to envision, and that is what makes it a possible hidden gem. The hidden-part is sure, while the gem-part remains to be seen. It will take many years to produce revenue, but once people start to see the potential and to talk more about it, the price will likely appreciate. I think I have to buy some. The price is at it's lowest.
You certainly deserve more upvotes. This was a very enlightening article.
Tau itself is written/created in C++ because Tau is a compiler. All programming languages have compilers. All compilers must be created in an existing programming language. This would mean the Java virtual machine cannot be created in Java. This would mean the Rust compiler cannot be created in Rust. This would mean C cannot be created in C, because you have to program the compiler in a stand alone language to implement it.
As a result the first implementation of Tau will be the C++ implementation. The C++ implementation does not have to be the only implementation. A Turing complete programming language must be used to implement Tau because according to my understanding you cannot put the constraints there. The constraints have to come in after the logic is put in place which happens in the compile process itself not in the compiler executable. This means Tau has to be programmed perfectly, and Tau itself will have to use correct by construction, which is actually possible to do with CompCert the verified C compiler. I do not know if you can do it using a C++ compiler but I know C and C++ aren't so different so someone could implement a C version of Tau with the verified compiler as long as Ohad releases a formal specification. I think also there is EscherTech which offers formal verification for C++ so Ohad might be able to use these tools to make an exact C++ implementation correct by construction.
References
Ok, so writing the compiler in C++ doesn't necessarily make Tau unpredictable. Thanks!
It's not impossible to write reliable code in C++. It's just very difficult to do it and even when you do you have the problem where the more complex the code is the harder it is to audit. When you use correct by construction, and when your code is limited only to for example a compiler, then you can focus all community efforts on that. You have to trust fewer programmers and fewer auditors when you use correct by construction and build the compiler only in C++ and do the rest in Tau.
In specific the consensus on heartbleed is that it was caused by lack of bounds checking. This would indicate that language security may have prevented heartbleed from happening. This doesn't mean mistakes cannot be made but it only means it's much harder to make them with certain languages.
My point by bringing up heartbleed is to show that if you use a notoriously difficult language for secure programming like C or C++, and you do not take all possible efforts to make sure your code is correct, such as correct by construction, formal verification, and all sorts of blackbox testing, then it's a situation where perhaps the entire world has to have faith in the competency of in some cases thousands of different programmers. The statistics do not look good when you consider that it only takes one of them to slip a bug in either deliberately or by accident.
References
https://en.wikipedia.org/wiki/Bounds_checking
https://news.ycombinator.com/item?id=7548991
Damn .. This is some hard core original content! Nicely done
The recent events with #thedao made this more relevant than ever!
Great piece and spot on.
The rise of OO the final tipping point that moved the industry in the bad direction. The old languages like Lisp, ML and Haskell have stayed around in the background while people departed for the bright lights of the "easier" OO.
Now things are starting to swing back again, Functional Programming is on the rise everywhere as people realize what they loast with OO.
Now many OO languages are starting to get Functional language features. Such as C++ 11, Java 8 and C# 3.5 onward.
I can't think why anyone would pick OO for blockchain, the entire nature of blockchain just screams functional code from its very core.