Earlier quoted context omitted.
Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it. I’d wager a million gazillion bucks that this is not the case.
So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?
Of course some bugs in Lean may exist (I don’t have deep insight into Lean’s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof.
As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I’d be very surprised if any buffer overflows or stack overflows exist.
Such overflows are not difficult or expensive to detect, so if any were there, it should cause a crash instead of an incorrect result.
It’s not as in handwritten C where you can forget or omit a bounds check.
I’d say it is even less likely than seeing an overflow in the Core of Java cause an incorrect result (i.e. corruption instead of a crash) - because Lean uses the De Bruijn principle of reducing to a very small Core, that is easier to keep correct (others in this thread have expanded on this I better than I can I think).
Out of pure curiosity: Do you believe otherwise or have a reason to think I am mistaken?