Let Lisa be a programmer and Bart be a business man. Bart would like Lisa to develop a software for his business. Since they don't previously know each other, they naturally ask themselves how they can trust the other party. Bart would like to pay when the program is ready and working, and Lisa would like to get paid before she even begins her work, so it won't turn out she worked for free. It will be fair to agree somewhere in the middle, like defining milestones, but this does not completely solve the trust issue, only roughly reducing it somehow. How can decentralized applications solve this trust issue? We have the Blockchain algorithm that removes the need to trust in many cases. On Bitcoin, one can supply a proof of coin ownership in a form of cryptographic signature, which allows them to spend those coins. Can this approach help Bart and Lisa? Blockchain could help only when given one vital property. Less a property of the blockchain and more a property of the code itself, and this goes back to a more basic question: when Bart gets to put his hands on the code, how can he know it works as he expected? Software verification/testing/quality-assurance is a major part of a software's lifecycle. It is not full-proof: we see buggy software everywhere, whether those bugs are misalignment against the original requirements of what the software should do, or security holes, or unexpected behavior. Making a quality software is a long, expensive, and speculative process with painful convergence rates. Computer scientists knew long ago that this situation is due to the logical nature of our programming languages themselves. Things were wonderful if we could only express formally the desired software's requirements, and the computer will be able to tell whether a given code meet those requirements. In fact, this turns out to be possible if we pick a subset of the programming languages called Totally Functional Programming Languages (TFPL). Given a code in TFPL, the provable assertions about it are exactly the correct assertions about it. Therefore, it is always possible to supply a proof, together with the code, that it meets certain requirements. That is not the case for Turing complete languages, as described briefly on my previous post. So, Lisa can write the program in TFPL and Bart can verify that the program meets his requirements. He will still have to hire a programmer to write those formal requirements (at least in many cases), but obviously expressing the requirements is much less hard that meeting those requirements. We have therefore solved the verification problem, but what with the payment-trust problem we began with? Solving this code-money chicken-egg problem is one feature that Tau-Chain will provide soon. Tau is a TFPL language; it gives TFPL meaning to existing languages (RDF family which are extremely human readable). Tau client is also a theorem prover and verifier, so it can prove assertions about a given Tau code. It also functions as a full blockchain node, but proofs can be simply any proofs at the mathematical sense, up to tau's typesystem (which covers all finite turing machines, hence virtually all possible kinds of computers). So, Bart could lock some coins in a multisig address with Lisa (that's like a Bitcoin's equivalent to a shared bank account requiring both signatures), and give a rule on Tau that the coins will be released to Lisa only if she supplies a proof that her code meets the desired requirements. Such proof will be verified by the whole network so to speak (or by "miners", the specific form is again up to the user's rules and how that specific coin over tau is built), and Lisa will trustlessly be rewarded the coins she deserve. It also worth mentioning that Bart can be sure that Lisa didn't hide any surprises in the code: he can automatically verify that the code is not doing things it should not do, like accessing private data. We are therefore entering a new era in the software world, where software can really be trusted, and humans can trust each other on a much wider variety of transactions. Sounds hard? We already finished developing a very powerful prover and perform a lot of tests over it. It didn't break yet, but we keep testing. It needs a bit more development to go beyond an RDF reasoner into a full Tau node: we have to finish the type system constraints, finish DHT&Blockchain builtins, write the genesis block, and voila! |

Blog >