Enjoyed the show very much. One comment: since Gary seems concerned that there are undecidable problems in the static analysis of Python, he may need to be aware that type checking in the ML type system that he seems to endorse so strongly is complete for EXP time. Which means neither works in a worst case sense, but it seems they both work enough in practice. Unfortunately theoretical analysis, which is largely worst case analysis, has shown time and again quite a gap from reality (the simplex is a practical worst case exponential algorithm, whereas there aren’t so many n^10 algorithms in practical use). This happens because the infinite set of slow or undecidable instances for a problem may be a negligible fraction of possible instances. Another observation about type systems is that they allow to check some, not all, interesting properties of a program at compile time in exchange for a certain loss of expressivity, that is additional lines of code needed to express a computation. This is simply because the shortest possible expression of a computation may not type check. This is also observed in practice looking at projects in different languages. The evidence that statically typed languages have fewer bugs per line is weak if it does at all exist, even if it stands to reason that if type checking excludes incorrect computations before they run, it should be helpful. So it is a trade off between the useful constrains one adds to a program to be statically less buggy and the additional verbosity required by type checking. The java.array.util library used to contain this comment: “The code for each of the seven primitive types is largely identical. C’est la vie.” That’s a blatant example of type checking and efficiency requirements (the arrays are “unboxed”, no pointers) causing a 7x code bloat. As Gary said, don’t look at Java, but the ML type system is EXP-time complete. That can’t be good either. The alternative is to check properties at run time with assertions. This is infinitely easier but it can cost in execution time an cause crashes in production. Complement with randomized testing, and you have the best of both worlds: simple property checking on concrete data, not types, and catching most errors before production. It seems to me the sw world is slowly voting with its keyboards for this approach.
https://www.podcastinit.com/destroy-all-software-with-gary-bernhardt-episode-159/