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)

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.

Thanks for sharing, those were great reads!

On expressiveness, people often frame it as a dynamic-language goal, but a large portion of type system research is precisely about making type systems more expressive so they can describe a wider range of programs and invariants. This is clearly something both camps value. I suppose another interesting benchmark could be: how do coding agents perform across languages with different degrees of type-system expressiveness?

We may directionally agree, but it is hard to draw conclusions without measurements. Overall, I'd say this is much more of an open question than people give it credit for.

Author here.

Type systems restrict which programs can be expressed and increasing expressiveness often requires increasing type-system complexity (which, speaking from experience, both humans and agents will struggle with). Plus they are not the only mechanism to assert correctness (they only validate a subset of your program correctness and do not replace tests) and you are still on your own when it comes to actually recovering from unexpected errors (something Erlang/Elixir were designed for).

I'd say there are two flip sides to your question:

1. Given types do not replace tests, if you can use AI to automate full test coverage, are there actual benefits in static typing for coding agents? The downside of tests for humans is that we suck at writing them (but guided agents can do better) and they can take time to run (which agents do not care)

2. Do we actually have any data or evaluations that show which typing discipline is better for agents? The only benchmark I am aware of [AutoCodeBenchmark] has Elixir come first (dynamic) and C# as second (static), so it doesn't answer the question. There are other benchmarks that show dynamic languages require fewer tokens to solve problems (but that's not a metric I particularly care about)

My gut feeling is that local structure, documentation, quality and quantity in the training data, etc are likely to play a more important role than typing for coding agents. I'd also love to measure how agents perform on specific domains. If you are writing concurrent software, how does Elixir/Java/Rust/Go compare? But without data, it's hard to say.

[AutoCodeBenchmark]: https://github.com/Tencent-Hunyuan/AutoCodeBenchmark

I maintain more than 20 packages and, except for the major ones, like Phoenix and Ecto, they haven't been updated in more than a year and yes, they are all fine.

The language has been extremely stable. There has been almost no breaking changes in over a decade. Case in point: we introduced a whole gradual type system without making any changes to the language surface! The language is still on v1.x!

You are commenting as if we added this now but we have made no changes to the language surface. The difference is that we now leverage these same language constructs to extract precise type information.

Comments URL: https://news.ycombinator.com/item?id=46557923

Points: 14

# Comments: 2

Comments URL: https://news.ycombinator.com/item?id=46049170

Points: 5

# Comments: 0

The idea that Phoenix is also mostly macros does not hold in practice. Last time this came up, I believe less than 5% of Phoenix' public API turned out to be macros. You get this impression because the initial skeleton it generates has the endpoint and the router, which are macro heavy, but once you start writing the actual application logic, your context, your controllers, and templates are all regular functions.