Conversation

Notices

1. Embed this notice
   Paul Cantrell (inthehands@hachyderm.io)'s status on Thursday, 09-Nov-2023 04:22:10 JST Paul Cantrell

   @jrose
   I’m totally with you on this. Every form of static verification has •some• horizon past which it either can’t reach at all or becomes too onerous to be worth it, and how far out that horizon reaches is not as important as how ragged its boundary is. You want the domain of a static type system to be something you can reason about cleanly, something that innocent refactorings aren’t constantly wandering across, and static types without generics just ain’t that.

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Thursday, 09-Nov-2023 04:23:54 JST Paul Cantrell

     in reply to

     @jrose I think part of the long-term appeal of dependent types is their Golden Hammer promise that this family of tradeoffs doesn’t have to exist, that this horizon can extend to infinity. I’m…skeptical. Good and fascinating things there, but I’m not going to bet in favor of that grandiose promise.

   • Embed this notice
     Ben Lings (ben_lings@hachyderm.io)'s status on Thursday, 09-Nov-2023 06:26:01 JST Ben Lings

     in reply to

     @inthehands @jrose I don’t believe any type system can extend this horizon to infinity. There will exist correct programs that can’t be proved correct within the type system. (Waves hands in the general direction of Gödel and https://perl.plover.com/yak/CHI/)

   • Embed this notice
     Paul Cantrell (inthehands@hachyderm.io)'s status on Thursday, 09-Nov-2023 06:30:05 JST Paul Cantrell

     in reply to

     • Ben Lings

     @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.