Semantic Smart Contracts and Investment Management
Verification and Audit of Crypto Projects
The problem of audit and verification of projects is more pressing to crypto funds than it is to individuals, as individuals take responsibility for their own assets only. In the case of funds, their shareholders shift the problem of project estimation onto the fund, and so the fund bears the whole lot of responsibility to every investor.
Advantage in the competition will belong to a fund that not only promise better profits, but is better in assessment of projects and risk management. The fund that is able to firmly control the project at every stage of its development.
Since we talk about crypto projects — a distinctive sphere — we cannot dispense with technical tools of management. The standard approach here is usage of smart contracts. The first concept of smart contacts was suggested by Nick Szabo in 1994. Bitcoin adopted some smart contract principles, but they were absent in the client software, for security reasons were not Turing-complete, and did not find practical use. Full-blown smart contracts first appeared in Ethereum.
Today smart contracts only have a narrow field of application. Their primary use is issuance of tokens and effectuation of transactions. Nevertheless, smart contracts can find a use in full or in part in automated project verification and audit. For instance, accounts on financial results, control of bargain terms, or funds distribution.
Those funds that succeed in implementing automated verification and audit will be able not only to manage bigger investment portfolios, but do it more efficiently.
Smart Contract Language Problem
Verification of smart contract based projects proves to be a difficult problem, if you use procedural or functional languages (the languages that are known as Turing-complete).
The problem originates from the known Gödel’s incompleteness theorem, which, applying to algorithm theory, indicates that no possibility exists to create a program that can predict execution of another program.
In other words, programming languages for smart contracts can turn out complex and convoluted. The history of Ethereum proves it. Cases are known when errors in smart contracts led to unpredictable results of transactions and projects. Errors occurred in EVM virtual machine for Solidity language. Due to complexity of the language in Ethereum they practice external audit, whereby experts analyze the code and make a decision whether the smart contract approximates to what the project should result with.
This is far from what crypto funds, crypto investors, and the whole crypto community wants. Ideally, the code of a smart contract should be friendly to the human eye and allow automatic verification prior to execution.
We propose to solve the verification problem at the conceptual level.
For smart contracts we need to choose a language of such a class as to be able to automate verification in full or in part. And, if automated verification fails, a human should be able to interfere and solve the problem in a predictable time.
In pursuing this goal, we consider the Theory of Executable Specifications (another name is the Theory of Semantic Programming/Modelling) to serve best. The theory was developed in the Institute of Mathematics, Siberian Branch of Russian Academy of Science in 1980s-90s by academicians Y. Yershov, S. Goncharov, and D. Sviridenko.
They described the method of building programming language classes based on Constructive first-order predicate logic. Such a language is close to the terminology of a given problem domain and thus can be easily understood by specialists, and on the other hand it is not only executable, but has an effective executable semantics (automated translation to an executable algorithm).
Such languages permit of automated verification for consistency. Also they are free from the halting problem[1]. This allows not only to verify smart contracts for consistency, but build and verify for consistency hierarchies of smart contracts.
It is quite possible to set rules under which the fund should operate (the basic terms) in the form of a smart contract. With adding new contracts to the portfolio, their smart contracts undergo automated verification for consistency with these rules.
Moreover, we can formulate the terms of a contract/bargain using the language that is customary in a problem domain. For instance, if the problem domain is warehousing, such words as stock, storekeeper, schedule, unload, etc. become the part of the smart contract. This language is easily understood by a human. E.g. a worker is able to see that before dispatching a batch to the buyer, they expect a payment confirmation. Accountants and legal officers are able to read smart contracts the same as traditional written agreements.
Scientists call this class of languages semantic languages. These languages are logical from the syntax point of view and, at the same time, are constructive, as they have procedural semantics. But, these languages are not so called “Turing-complete”, because they have certain limitations (e.g. they limit use of negation operations and unrestricted quantifiers (cycles) in certain syntactical situations).
By abandoning Turing completeness, we acquire a human-friendly language that can also be automatically verified. However, we do not sacrifice functionality. The power of semantic languages is quite enough to handle complicated relations within a project, as well as compute transactions.
The same way semantic languages can be applied to automation of audit.
Semantic smart contracts can describe rules of a fund and an agreement between the fund and a project. There are several benefits here. Firstly, as it was described above, automated consistency check can be implemented. Secondly, the halting problem goes away automatically. Thirdly, thanks to similarity of the smart contract language syntax to that of the problem domain terminology, investment managers with the knowledge of the said problem domain can easily verify that the purport of the smart contract is the same as that of the paper contract between the project and its investors.
Finally, we would like to note that semantic languages are not a pure theory. We actively work on projects in this area and will present first results soon.
[1] Halting problem is the problem whose solution employs Gödel’s incompleteness theorem. Semantic languages solve the problem on the syntax level, by reducing syntax of the language, making it effectively non Turing complete, but still leaving enough expressional power.
