wizzwizz4 (wizzwizz4@fosstodon.org)'s status on Monday, 13-Jan-2025 10:18:15 JST

@alilly @alcinnz That said, if you're willing to go really eccentric, the minimum you need is a LISP model of the CPU (including the instructions you want to support), a proof system, and a basic constructive compiler. Then, if you want more optimised machine code for something high-level, you can prove the equivalence of the two algorithms (up to the extent your LISP is supposed to preserve lower-level semantics).