I don't think these articles fully cover (pun intended) the claims being made.
First of all, we need to separate "types" from "static type checking". Elixir always had types and types by themselves won't eliminate tests. You can combine types with type checkers, as well as tests themselves (as described in the first article), to aid software verification. Plus many of the techniques discussed in the article (property-based testing, static analysis, etc) are available to dynamically typed languages too.
Some notes on the first article:
> For example, there is no test we could write that would show that our function never throws an exception or never goes in to an infinite loop, or contains no invalid references. Only static analysis can do this.
Static analysis is doing a lot of heavy lifting here. When applied to type checking, where it can prove absence of exceptions depends entirely on how expressive the type system and checker are.
For example, this Haskell function can fail at runtime even though it type checks:
maxPosInteger :: (Ord a, Num a) => [a] -> a
maxPosInteger xs = maximum (filter (> 0) xs)
If `xs` contains no positive elements, maximum fails. The type system does not rule this out.
As the article itself later discusses, proving stronger properties requires more expressive type systems, such as dependent types. Those systems can prove the absence of additional classes of failures, but they come with their own costs in complexity, ergonomics, inference, compile times, and so on. My recent ElixirConf talk touched on these trade-offs: https://www.youtube.com/watch?v=Ay-gnCqDw9o
But overall the article does not discuss coverage. Under some of the scenarios it presents, such as finite domains, exhaustive testing guided by coverage can prove the absence of bugs too. Additionally, some of the concerns the article has about Python, such as runtime redefinition and excessive polymorphism, do not really apply to dynamic languages like Elixir and Clojure.
> Correctness oracles abound. We have test suites, fuzzers and property-based testers, runtime sanitizers, static analyzers, linters, strong type systems, and formal verifiers. Any time such a tool can be made available to the LLM, we’ll reap the benefits in terms of not dealing with bugs the hard way, later on.
I completely agree with that framing. Static type systems are valuable tools, but they're one tool among many. My overall point is that I wouldn't draw the line at static typing as the "must have" mechanism for software quality, especially in the context of AI-assisted development where multiple correctness oracles can be composed together.
I actually think an land value tax is our best option, it's just that a land value tax still allows for housing as investment. To make housing not an investment you need to eliminate returns from housing altogether.
Yes, obviously I think that having a 100% capital gains tax on housing would be pretty absurd, and would not lead to the types of outcomes we actually want. We often do want developers betting housing, which incentivizes improvements and reselling the places. But my point here is that -- for those who truly want housing to not be for speculation -- you need to completely eliminate economic gains from buying housing. They way you do that is to tax the capital gains that come from the sale of housing to the point where they no longer exist.
A land value tax is probably the best option for what we want to happen which isn't "eliminating speculation" but is instead to prevent land hoarding. We actually want people to speculate on properties, but in doing so, to develop them in to efficient uses if that future value.
Types are also documentation!
They also decrease the degrees of freedom LLMs have to make mistakes [1].
[0] https://kevinmahoney.co.uk/articles/tests-vs-types/
[1] https://john.regehr.org/writing/zero_dof_programming.html
reply