Re: Andrej Bauer gave an extraordinarilly clear talk

[Tim Daly]

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 <axiomcas@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 <avigad@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 <axiomcas@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
>>>
>>
>