Here’s something all statically typed languages miss out on. I don’t want a type checker, I don’t want some rigid construct telling me my code is incorrect. Even when I’m mixing up addition for strings and integers by trying to add one to the other the type checker needs to get out of the way because maybe I actually do want that to be a runtime exception since the general data flow is correct and worrying about clients supplying me a string instead of an integer is more hassle than it’s worth and the failure happens at a safe point in the computation.
What I want at the end of the day is something that can reason about all the code I’m writing without enforcing a static discipline. I want something that will tag certain parts of the code as “unreasonable”, not type correct or type incorrect. Unreasonable being something that is hard to analyze in terms of what kinds of data types are flowing through those parts of the code. In the above example when I was adding a string and an integer incorrectly this analyzer should have marked the addition as unverifiable and then traced the data flow to the point where the inconsistency was introduced instead of barfing “can’t add string and integer”. Yes, I know you can’t add a string and integer. Tell me something I didn’t know already. Show me where the data flow went wrong and at which point the data became “unreasonable”. It might be a bug in my code or maybe it is something I intended all along. The tools must always be subordinate to the programmer’s intentions. Not the other way around.
Extend this idea to more than data types. Let me reason about the garbage collection profile of my program. Show me guesses for allocation and deallocation at various points in the program. If something is again “unreasonable” as in it is hard to tell how much memory will be required to store a certain object coming over the wire then that again might be an error in my code or maybe I know an upstream system will never be able to send me more than 2kb of JSON and so it is safe to assume no excess garbage will be generated. Again, the folks designing Rust came at it from the wrong angle. They built a static system backed by logic instead of building a code reasoner to help the programmer.
Further yet. Show me the phases of what the compiler will do. Maybe there is a missed opportunity for inlining something and I don’t want to drop down to C and assembly to manually inline the code. JITs and other compiler technology are great but they are black boxes and at the end of the day you end up guessing and checking what exactly the JIT will do to make your program performant. So show me all the spots where inlining is going to happen. It doesn’t even have to be accurate. Just a close enough approximation for me to reason about it.
So really what I want are auxiliary reasoning modules for my untyped code. I believe the professionals call this kind of thing an abstract interpreter. All modern compiler technology is built and optimized for compiler writers to transform trees into other trees or linear sequences instead of being designed and optimized for programmers to reason about and validate the intentions they are translating into code by plugging together composable abstract interpreters. What I want is a set of composable tools to elaborate high-level descriptions of computational intent into executable machine code but instead what I have are rigid barriers constructed by others who think they know better about what intent I have with writing a piece of code and I am forced to squeeze whatever I had in my head into some logical peephole called a type system. Most of modern software development is broken because program correctness is placed above program reasonableness when it really should be the other way around.