It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statemen

It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statements about e, what does the system look like? It turns out that if you have that system in code written as s and then try to assert certain properties of it G, then it’s possible to design G such that s: G is so twisty and self-referential that it can’t be verified. Something to that effect: strong logics have a tough time speaking completely about themselves. So that’s at least one property for one program that’s unprovable no matter how powerful our type system is. But that’s so long range. Practically we can make type systems that let us prove massive amounts of things using judgements like e: B. The real issue is that it’s just very hard and expensive to make those systems practically eliminate even a small subset of bugs.