Абмеркаванне

@vitaut is it the fact you're dealing with IEEE whatever whatever floating point that makes lean useful or could there be uses of it that might be helpful in other realms, such as the kernel?

I suppose something strictly mathematical lends itself well to it better than usual code :)

Jula Lawall (who's great) has given a talk on formal verification in the kernel, e.g. this one at KR - https://kernel-recipes.org/en/2025/schedule/program-verification-for-the-linux-kernel-potential-costs-and-benefits-tentative/ - that seems to ultimately conclude (in my view :) that it's really not all that practical except for perhaps very specific parts of it.

But I wonder if lean changes things in any way... :)

@ljs I am sure it can be made useful in other domains as well, maybe proving some concurrent algorithms or even lifetime guarantees.

@vitaut

I wouldn't call this normal. Such improvements sound like to opposite of 'subnormal' 😎🤘

@DanielaKEngert supernormal?