A Survey on Security Verification of Blockchain Smart Contracts <s> 2) DEVELOPING NEW CONTRACT LANGUAGE <s> While procedural languages are commonly used to program smart contracts in blockchain systems, logic-based languages may be interesting alternatives. In this paper, we inspect what are the possible legal and technical (dis)advantages of logic-based smart contracts in light of common activities featuring ordinary contracts, then we provide insights on how to use such logic-based smart contracts in combination with blockchain systems. These insights lead us to emphasize a fundamental challenge - algorithms for logic approaches have to be efficient, but they also need to be literally cheap as measured within the environment where they are deployed and according to its economic rules. We illustrate this with different algorithms from defeasible logic-based frameworks. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) DEVELOPING NEW CONTRACT LANGUAGE <s> Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Ethereum's EVM, while avoiding some of the problems they face. Simplicity comes with formal denotational semantics defined in Coq, a popular, general purpose software proof assistant. Simplicity also includes operational semantics that are defined with an abstract machine that we call the Bit Machine. The Bit Machine is used as a tool for measuring the computational space and time resources needed to evaluate Simplicity programs. Owing to its Turing incompleteness, Simplicity is amenable to static analysis that can be used to derive upper bounds on the computational resources needed, prior to execution. While Turing incomplete, Simplicity can express any finitary function, which we believe is enough to build useful ``smart contracts'' for blockchain applications. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) DEVELOPING NEW CONTRACT LANGUAGE <s> Blockchain platforms, such as Ethereum, promise to facilitate transactions on a decentralized computing platform among parties that have not established trust. Recognition of the unique challenges of blockchain programming has inspired developers to create domain-specific languages, such as Solidity, for programming blockchain systems. Unfortunately, bugs in Solidity programs have recently been exploited to steal money. We propose a new programming language, Obsidian, to make it easier for programmers to write correct programs. <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) DEVELOPING NEW CONTRACT LANGUAGE <s> Blockchain-based platforms such as Ethereum support the execution of versatile decentralized applications, known as smart contracts. These typically hold and transfer digital currency (e.g., Ether) to other parties on the platform. Contracts have been subject to numerous attacks, losing hundreds of millions of dollars (in Ether). We propose Flint, a new type-safe, capabilities-secure, contract-oriented programming language specifically designed for writing robust smart contracts. To help programmers reason about access control of functions, Flint programmers use caller capabilities. To prevent vulnerabilities relating to the unintentional loss of currency, transfers of assets in Flint are performed through safe atomic operations, inspired by linear type theory. <s> BIB004 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 2) DEVELOPING NEW CONTRACT LANGUAGE <s> Smart contracts enable autonomous decentralized organizations (DADs) in large, trustless and open trading networks by specifying conditions for automated transactions of cryptographically secured data. This data could represent cryptocurrencies but also sensor data or commands to Cyber-Physical Systems (CPS) connected to the Internet. To provide reliability, the contract code is enforced by consensus and the transactions it triggers are nonrevertible, even if they were not intended by the programmer, which could lead to dangerous system behavior. In this paper, we conduct a survey over existing smart contract platforms and languages to determine requirements for the design of a safer contract language. Subsequently we propose concepts that enhance the understanding of code by limiting confusing language constructs, such as nesting, arbitrary naming of operations, and unreadable hash identifiers. This enables human reasoning about the contract semantics on a much higher abstraction layer, because a common understanding can be derived from the language specification itself. We implement these concepts in a new domain specific language called SmaCoNat to illustrate the feasibility and show that our concepts are barely covered by existing languages but significantly enhance readability and safety without violating deterministic parsability. <s> BIB005
Developing new contract language is an effective way to write the correct smart contract. A variety of programming languages such as Idris  , Simplicity BIB002 , Obsidian BIB003 , and Flint BIB004 have been proposed. These Type-based functional languages make the development process safer. Through the static analysis of smart contracts, we can more easily find vulnerabilities in the writing process which reduces the generation of contract errors and testing requirements. In addition to the programming languages mentioned above, Idelberger et al. BIB001 proposed a smart contract based on logic language, pointing out a new idea. The complement of logical language and programming language can make the design of smart contracts clearer. Regnath and Steinhorst BIB005 proposed a new programming language, SmaCoNat, which was a human-readable, security, and executable language. They converted programming language grammar into natural language sentences, such as directly giving names to variables instead of directly using memory addresses, which improved program readability. At the same time, to improve the security of the program, they reduced the possibility to repetitively alias logic and data structures by custom names.