I think "bad at specifying the domain and range of functions" was somebody trying to describe type safety in more pedestrian terms.
I think the actually idea is while the theory of statistics (like all math) is well typed, professional statisticians tend to use shitty tools/programming languages without good type systems.
People scoff that type errors are easy, but when most of the work is encoding the domain knowledge, and the statistics isn't to bad and just the last step, you definitely want to make sure you model prior to drawling statistical conclusions is sound and rich.
tl;dr there's good reason to invest in better tools, and the homotopy type theory that's being funded is as much about "how to apply math" as "what math to apply".
No, it is not about static typing or the general use of typed data structures for describing statistical software. Statistical software has been among some of the best software around for a long time. In fact, I frequently revisit aspects of the C++ implementation of STAN and the interface design of pymc as inspiration for effective software design in other domains.
The idea that statistics is a field with poor software tools is just plain crazy.
> Stan interfaces with the most popular data analysis languages (R, Python, shell, MATLAB, Julia, Stata) and runs on all major platforms (Linux, Mac, Windows).
None of those languages have good type systems.
And like I said, this is about modelling more generally than just statistics.
I think the actually idea is while the theory of statistics (like all math) is well typed, professional statisticians tend to use shitty tools/programming languages without good type systems.
People scoff that type errors are easy, but when most of the work is encoding the domain knowledge, and the statistics isn't to bad and just the last step, you definitely want to make sure you model prior to drawling statistical conclusions is sound and rich.
tl;dr there's good reason to invest in better tools, and the homotopy type theory that's being funded is as much about "how to apply math" as "what math to apply".