Mastodawn

Regarding Leo’s post, it was in poor taste but no poorer than anyone who knows him has come to expect. My comment is that I bet Lean is inconsistent too. I don’t know exactly where and how, all I am saying is that I don’t doubt it. These are very sophisticated pieces of software.

In fact, I don’t doubt that those working in the trenches of the FRO could point to some dark corners and examples of unpublicised sources of inconsistency.

This isn’t to dunk on Lean. Bugs can happen, and having a small kernel is a good way to limit their scope! But there are many ways for assurances to fail and this can happen inside and outside the kernel.

Show thread

Jon Sterling Mar 17

I am also not too impressed by the existence of second-party checkers in the context of a language that lacks decidable type checking. Because something has to give, these checkers will be (necessarily) incomplete in one way or another, most likely each in different ways. This is because lean’s failure of completeness of conversion almost certainly manifests in heuristic ways that are not predictable or replicable…

For a fail safe checker to provide confidence, it needs to be complete. This is not possible with Lean’s core language as designed, and it will not be possible for Lean itself until they find new leadership.

Show thread

RanaldClouston

@jonmsterling In his post he explicitly says "The checking is deterministic: run it again, get the same answer". Is there something I can read on why this is false? If it is false, why is he saying the opposite?

Show thread

Jon Sterling Mar 17

@RanaldClouston It is deterministic as far as I know. The issue is that if you are implementing a checker for a broken/incomplete system, there are a million different places where you can put the incompleteness, because syntactic invariants are like squeezing a balloon. When one is broken, you can sometimes make it hold but then another thing breaks. Because there is so much room for movement here, it becomes very difficult to even specify what it would mean to have an independent checker. Even if this is fully specified, which would be possible to do, the result would be of limited value in my opinion.