What is ULM?

The Pi Squared Universal Language Machine

Disclaimer: This documentation is preliminary and subject to significant changes as the product develops.

The Universal Language Machine (ULM) is an advanced, open-ended platform that enables developers to create, deploy, and interact with smart contracts written in any programming language. Unlike existing systems that require all contracts to be written in a single language, the ULM natively supports multiple languages. This allows diverse language ecosystems to coexist and interoperate on the same blockchain, empowering developers to use the most suitable language for their projects and broadening the accessibility of smart contract development.

By supporting multiple languages within a single blockchain, ULM addresses two fundamental barriers in blockchain development:

1. Improving accessibility to Web3 and blockchain-based development

2. Enhancing interoperability across different programming paradigms

The ULM leverages formal semantics of programming languages to execute contracts, ensuring correct-by-construction executions that result in correct and secure smart contract operations. ULM is powered by the K framework, a proven system for formally defining programming languages backed by decades of research and extensive industry use.

This advancement significantly improves flexibility, developer experience, and security. It also paves the way for future innovation in decentralized applications, fostering a more universal approach to blockchain programming.

The ULM is a universal blockchain execution layer powered by the K framework that allows developers to build and interact with smart contracts written in any programming language. This includes both currently supported languages and languages developers may introduce to ULM. It achieves this by directly integrating custom formal language semantics into the blockchain without using or introducing compilers. The ULM operates as a modular system, where each supported language is captured as an independent formal semantics module in K, referred to as a "language module."

Each language module is a formal specification of the language's syntax and semantics. K executes this module directly without intermediate compilation. This guarantees correct-by-construction execution: as long as the semantics are correctly specified, the execution will be correct. K acts as a mathematical prover that produces formal proofs of correctness during execution. When a contract is deployed or called, the ULM determines the correct module to execute the contract's code based on an identifier associated with the language's semantics. This design allows contracts in different languages to coexist, call each other, and even perform operations across language boundaries on the same global state. ULM supports a fully extensible architecture that enables new languages to be added dynamically and fosters continuous smart contract development innovation.