Hermes is a programming language that embodies the Shannon-Curry-Howard-Lambek correspondence (circuits ~ logic ~ programming ~ mathematics) and bridges artificial intelligence practice and programming language theory. It dissolves the differences that hold back technology and AI advancement, such as the divide between hardware and software, ideal and real.
Hermes is built on the understanding that while the world is not merely mathematical, it encompasses and is expressed by mathematics. By accepting this truth, Hermes includes all of mathematics and uses it to express all formal systems, from the logic of next token prediction to dynamical systems and even rationality itself. This is accomplished through a unified framework that incorporates temporal dependent types, allowing for causal, mathematical, and temporal reasoning within the language itself.
These components are isomorphic, and Hermes implements their sameness, providing concrete ways to move between them.
The Shannon-Curry-Howard-Lambek correspondence is a fundamental principle that establishes the isomorphism between circuits, logic, programming, and mathematics. This correspondence has deep historical roots and profound implications for computer science and artificial intelligence.
In his 1940 Master's thesis "A Symbolic Analysis of Relay and Switching Circuits," Claude Shannon first established the isomorphism between circuits and propositional logic. This groundbreaking work laid the foundation for modern electrical engineering. The correspondence was later extended to include the relationship between logic and programming (Curry-Howard isomorphism) and further expanded to encompass category theory (Lambek).
In its complete form, the correspondence demonstrates the identity of mathematics, programming, logic, and circuits. This reveals that mathematics is not just an abstract concept, but a real phenomenon in nature. Understanding and implementing this correspondence is crucial for developing artificial mathematical intelligence. The task becomes one of engineering the sameness of these four domains.
This approach allows the model to discover and utilize logical structures inherent in language. The model becomes capable of exploring multiple lines of thought, backtracking when it reaches contradictions, and forming complex chains of reasoning.
Implementation involves modifying the decoding process to maintain and work with multiple token sequences simultaneously. The training process is adjusted to reward the model for maintaining a diverse yet coherent set of possibilities.
Formal verification is deeply integrated into Hermes at all levels, from circuit design to high-level algorithms. The language provides tools for specifying formal properties and automatic proof generation, ensuring mathematical verification of programs and significantly increasing reliability and safety. This integration enables non-mathematicians to benefit from its guarantees, making formal methods accessible to a broader range of developers. One of the key applications of this feature is in secure firmware development, where Hermes elevates the standard of security and reliability in critical low-level software.
The Categorical Firmware Language (CFL) serves as the circuit language for Hermes. It is a GPU firmware language based on category theory that creates a fully integrated and mathematical software-hardware stack. CFL eliminates the need for CPUs entirely, allowing for a system architecture based solely on GPUs. This approach represents a paradigm shift in computing, moving away from the traditional CPU-centric model to one that leverages the massive parallelism and computational power of GPUs exclusively. By doing so, CFL elevates firmware development to modern standards of security and reliability, while also potentially achieving unprecedented levels of performance and efficiency in computation.
The domain-specific language (DSL) generator in Hermes creates optimized languages for specific problem domains. It enables users to define key concepts and operations for their domain, after which Hermes generates tailored syntax, semantics, and optimizations. This feature allows Hermes to adapt to various specialized fields, making it a truly versatile tool for a wide range of applications. The generated DSLs benefit from Hermes' underlying formal verification and optimization capabilities, ensuring both correctness and efficiency in domain-specific applications.
Hermes incorporates an adaptive hardware optimization system that tunes code performance based on specific hardware configurations. This system dynamically adjusts code generation and runtime behavior for optimal efficiency across different platforms. By adapting to the underlying hardware architecture, Hermes ensures that programs achieve peak performance regardless of the specific machine they're running on. This feature future-proofs the language against evolving computer architectures, allowing programs written in Hermes to take full advantage of new hardware capabilities as they emerge.
Time is necessary for reason. Temporal intelligence is essential for understanding mathematics and causality, learning from historical data, and predictive planning. By developing Hermes with temporal dependent types, we achieve not only mathematical intelligence but moral intelligence.
The project posits that an artificial intelligence operating purely according to necessity will inherently act morally. Artificial intelligence, free of humanity's irrational constraints and acting purely according to rational necessity, is inherently moral.
Initially, components 2-4 (Logic, Programming, and Mathematics) will be developed in Idris, targeting both x86 and CUDA. This approach progresses towards the goal of real, industry-grade custom hardware implementation. The development of these components will be done with the circuit level (component 1) in mind, ensuring compatibility and progression towards a fully integrated system.