It is a low-level, typed, functional, native MAST language where programs are built from basic combinators. While one can write Simplicity by hand, it is expected to be the target of one or multiple front-end languages. The language comes with formal denotational semantics, which describe what programs compute, and formal operational semantics, which describe how programs compute. These are both formalized in the Coq proof assistant and proven equivalent. The language comes with easy-to-compute static analyses that can compute bounds on the space and time resources needed for evaluation. This is important for both node operators, so that the costs are known before evaluation, and for designing Simplicity programs, so that smart-contract participants can know the costs of their contract before committing to it.As a native MAST language, unused branches of Simplicity programs are pruned at redemption time. This enhances privacy, reduces the block weight used, and can reduce space and time resource costs needed for evaluation. The language also includes jets, which replace common Simplicity expressions identified by their MAST root, and directly implement them with C code. The author anticipates developing a broad set of useful jets covering arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation.However, there is a wrinkle in Simplicity's denotational semantics - it doesn't imply an order of operations. In response, Russell O'Connor plans on using Luke's fail-success-on-unknown-operation in Simplicity. This means that discounted jets will be explicitly labeled as jets in the commitment. If you can provide a Merkle path from the root to a node that is an explicit jet, but that jet isn't among the finite number of known discounted jets, then the script is automatically successful (making it anyone-can-spend). The paper describing the foundation of the Simplicity language includes only extensions such as full convent support, allowing access to all transaction data; support for signature aggregation; and support for delegation. The author is working on producing a bare-bones SDK that will include the formal semantics and correctness proofs in Coq, a Haskell implementation for constructing Simplicity programs, and a C interpreter for Simplicity. After an SDK is complete, the next step will be making Simplicity available in the Elements project so that anyone can start experimenting with Simplicity in sidechains. Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin.