You are presented with multiple paper abstracts, alongside the associated literature review and chapter titles. Given the provided information, you are going to do a literature review. Please generate a coherent literature review that synthesizes the content, draws connections between different works, highlights major findings, and identifies any gaps in the existing research.

Literature Review Title: A Survey on Security Verification of Blockchain Smart Contracts 
Chapter Title:  2) DEVELOPING NEW CONTRACT LANGUAGE 
1. Abstract of Cited Paper (BIB001):  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. 
2. Abstract of Cited Paper (BIB002):  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. 
3. Abstract of Cited Paper (BIB003):  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. 
4. Abstract of Cited Paper (BIB004):  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.

Literature Review:
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.