I gave some thought to the question of generating code from a LEAN proof. The same idea occurs in FPGA work.
Assume that LEAN generated code for the GCD. Assume it outputs the code and its associated proof. The proof also has the associated axioms and definitions. It should now be possible to hand modify the code to optimize it yet still maintain a valid proof state. The same situation occurs at the Verilog language layer for FPGAs. The Verilog language is compiled into a circuit implementation. Often the circuit implementation can be hand optimized. For example, the hardware might have a DSP (Digital Signal Processor, aka a fast arithmetic unit) built into the chip. The "verilog code generator" might not know about this circuit so the designer can hand modify the generated circuit to use the DSP. The circuit is simulated before and after the change. Signals from each are compared to see that they generate the same sequence of states, showing the equivalence. This raises two interesting thoughts about LEAN code generation. Thought 1: The proof code generation ought to create a state machine model of code, either Mealy or Moore machines. That allows clearly identifiable "states". So LEAN code would target a specific code execution model rather than a general purpose free-form non-model. Thought 2: Given a "LEAN code generated state machine" target, it would be possible to create "hand optimizations" to the code. These hand optimizations could be proven correct at the LEAN language level. These optimization proofs could then be added to the generated pile, creating both new code and a new proof. The new optimized proof essentially uses the original proof as an axiom. This creates a "stepping stone" to LEAN proof generation. Early proofs using a dirt-simple state machine model would generate proven correct code. An interactive "proof optimizer" could have a suite of proven transformations available for hand optimization. Example transformations might be "unwind a recursion into a loop", "unroll a loop one state at a time", "combine multiple states into a single state", etc. Can LEAN decide if a recursive proof is equivalent to a looped proof? It seems it could because both proofs would be able to calculate equivalent results as long as the "states in the proof" use finite descending sequences. Can LEAN prove that the recursive state machine and the unrolled loop state machine are equivalent? That is, can "optimization" code transformations be proven correct? Again, I claim it should be possible, given a state machine target model for generated code. I think Bob Harper had a NuPRL-like effort at some point. I vaguely remember mention of an effort at code generation. That was long ago so my memory is likely faulty and I don't remember the name of his effort. Anyway, LEAN code generation is an important step in the Axiom SANE research. If you know of any research in the community please let me know. Tim On 6/27/21, Tim Daly <axiom...@gmail.com> wrote: > I thought his example of linear behavior to be about > as clear of a proof construction as any I've ever seen. > You could look at his LEAN notation and almost > understand it even if you never saw it before. In fact, > his LEAN construction is almost Axiom code. > > I found his comment that "you're going to learn > a lot of mathematics you thought you knew" as being > accurate. Every time I think I know something I end > up on a journey learning math I thought I knew. Sigh. > > My head is much too small a place to do mathematics. > > The LEAN website ought to have a link to that talk. > > He made the comment that the programming community > is one of the largest consumers of the type technology. But > my experience is that the LEAN community is not particularly > interested in the programming community. I don't find > many tools or much effort focused on proving actual > programs correct. The focus is more toward the math > community, probably because Buzzard is pushing hard. > > Once I figure out how to get the proof checker running > in hardware on an FPGA I'll move back to the LEAN level. > I'm making good progress on this. It turns out that it is > possible to inject C++ code into the FPGA build stream. > If I were smarter I could just grab the LEAN sources. > > I really want LEAN to focus on program generation from > a proof. I want to point at the proof of the GCD, press a > button, and have running Lisp code, as well as the list > of axioms and definitions for a specification. My current > effort of "working backward" from the program to the proof > is clearly the wrong way to go. I think I might have to focus > on LEAN code generation when I have working hardware. > > Building Axiom from the LEAN proofs would change the > whole world. > > Tim > > Where are the graduate students when you need them? :-) > > > On 6/26/21, Jeremy Avigad <avi...@cmu.edu> wrote: >> Thanks for pointing this out to me -- I had heard about it. The Scholze >> post was huge for us. >> >> Best wishes, >> >> Jeremy >> >> >> On Sat, Jun 26, 2021 at 5:47 PM Tim Daly <axiom...@gmail.com> wrote: >> >>> Andrej Bauer gave an extraordinarilly clear talk >>> "The Dawn of Formalized Mathematics" >>> https://vimeo.com/567049015 >>> >>> It is, of course, painfully obvious to us but I think >>> it might be a good introduction for a class on Lean. >>> >>> Tim >>> >> >