Urbit does this cool trick where you use pure lambda calculus arithmetic (church encoding), use this theoretically correct impl as a basis of your proofs and re

Urbit does this cool trick where you use pure lambda calculus arithmetic (church encoding), use this theoretically correct impl as a basis of your proofs and reasoning, and then at runtime provide a polyfill that uses hardware arithmetic operators. The runtime impl is thus not equal since it can for example overflow, but in practice that doesn't inhibit our ability to make useful programs. https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding Facebook does this also with GraphQL - GraphQL queries are theoretically dynamic and defined by the client, but you can bake them when you ship, and then provide optimized implementations of the query that also have knowledge of the UI and database that they aren't supposed to otherwise have.