Embed Notice

@ben_lings @jrose You don’t even need to wave your hands as far as Gödel: the theorem that no static type system can be both sound and complete without being uncomputable does the trick.

AIUI (which is not very well), dependent type research makes the case that yes, while this is technically true, it is possible to cover the non-pathological cases we actually want for practical purposes if we just push the envelope of automated theorem provers far enough. That’s the thing I’m skeptical of.