[angry_octet]

The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler.

So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program.

There is also the problem of knowing whether the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.

[ekidd]

Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day.

So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actually proved what you think you did, and (2) all the stuff you were normally trusting anyway. (Some of the stuff you were trust anyway is broken, of course.) But this is a smaller problem than trusting 1,000 lines of highly-optimized CSG code written by a model we don't actually understand.

[angry_octet]

Oh yes, it is still a better situation. Although C compilers are quite buggy.

Since Lean can emit LLVM it might be more achievable to reach performant assembly without going via C. All sorts of interesting work in progress.

https://dl.acm.org/doi/10.1145/3192366.3192377

(I am rate limited to ~5 comments a day so not replying for ages is just a function of the HN gods on Mt Sunnyvale.)

[kens]

It's kind of hopeless to try to prove that a microprocessor works according to spec, since you're dealing with physical objects in the real world. For instance, early versions of Intel's 386 processor had a 32-bit multiply problem that only showed up in some chips under particular combinations of temperature, voltage, and frequency, probably due to a transistor that wasn't large enough to provide an electrical margin under worst-case conditions.

[angry_octet]

Chip makers would disagree. They use tools that simulate at the electrical circuit level for just such problems, and using massive amounts of testing and inspection to statistically bound variations in chip geometry caused by process variation.

It is the quantum effects that occur at tiny geometries that make this hard, but every chip you buy has passed extensive variation.

To account for individual variation and random glitches there are other techniques, like triple modular redundancy or lockstep processors. Or for less stringent software, just computing it twice in different cores and memory blocks.