Add formalized lean implementation with WIP browser build#29
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
So issue #3 has haunted me for a long time and I couldn't help but wonder if my interpreter had a bug in it. As a result, a long time goal of mine has been to formalize this interpreter in Lean which guarantees it's bug free. Turns out it was bugs in the FRACTRAN programs themselves and not my interpreter, after all.
This has been a long-term quest of mine, which all of a sudden I was able to prove from scratch in just one weekend vibe-coding with Claude Opus. It almost feels surreal. Anyway, here it is. I'm still working on getting the browser build up to standards but it's working right now.
The trick with the browser build is that Lean compiles to C code, so by linking together that C code with the Lean runtime and requisite C libraries like GMP, I can compile it for the browser without too much fuss. And of course, Opus handled all the fuss with grace.
I'm still working on benchmarking performance but it seems pretty good, similar to the Haskell interpreter. Once I have it stable and the web UI looking nice, I will switch over the browser build to that.
Are the proofs elegant? No, look at the size of
leap_correctlmao. I'm going to try to clean up these proofs later.