A brief analysis and discussion on formalist vs intuitionist progra...

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.

Logo of Ethereum
Logo of Tau

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

A brief analysis and discussion on formalist vs intuitionist programming factions in the crypto community.