> if you can use AI to achieve full test coverage, are there actual benefits in static typing for coding agents?

Full test coverage doesn’t tell you if the tests behave correctly. So you could prompt an AI agent to write 100% test coverage where those tests could be exercising all code paths yet contribute 0% to the story of what the code does. You need human understanding of what the desired contract is that the tests check.

Imagine a contract lawyer who blindly signs any contract that they are given: they aren’t doing their job. They ought to have an idea in mind of what their client’s goals and limits are so they can determine if a given contract fulfils those needs.

Types are a declarative contract, so they can be a lighter yet more limited way to enforce a contract. The compiler can verify if all the declared types across the program agree with each other. This is especially helpful with refactoring, such as ensuring the adding a field has been rolled out everywhere.

Types aren’t to be just checked by the compiler, but checked by the human authors too. That’s why explicit type signatures are valuable, especially if they are kept intelligible. They encode the different variations in state and possible branching on that state. So you can whittle your types down as a way of whittling the solution down to be more focused. The problem in your head is reflected in the types, and any simplifications in the types then simplify the problem in your head, and any tests derived from that understanding.

In my experience restricting programs that can be expressed is a good thing, even more so with agentic engineering. The more guardrails there are, strong typing/TDD/computer use/..., the solution space shrinks and chance of a robust solution increases. Sure maybe this burns more tokens going in circles but it feels less like a slot machine more like a robot searching for a solution for a well-defined problem.

Devs have very strong opinions about dynamically typed programming languages. But reasons such as "exploratory programming", "expressiveness", "taste" that makes them feel good to program in for humans does not matter for agents. Agents don't care that the language "limits them" and prevents them from expressing the code in a succint way because it would not type check.

>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)

This articulates a lot of my own thinking wrt type systems, speaking as a downstream user without a lot of exposure to prog language theory, and I wish this debate were more often framed in these terms.

Another reply to this comment hinted that it might be more about giving LLMs feedback loops and that to me also seems like a more likely mechanism.

I'm not an elixir user but I've watched it from a distance over the years – thank you for your efforts and your experimentation.

>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).

I used to hold similar opinion but D language, and this article by Patrick Li (HN JITX co-founder) who's the original author of little known but very powerful language Stanza changed my mind [1],[2].

He argued that Ruby has enabled a very expressive language that enabled RoR, and when it was originally written other languages are less capable, and accordingly the proof is in the pudding.

In his new language Stanza for his PhD thesis he has designed an optional typed system supporting both typed and untyped, it seems very similar in concept to the OP article that you've written on Elixir. Groovy also deserved a special mention, and the pudding is Grails.

Interestingly both Elixir and Stanza have GC, but Stanza also support non-GC namely LoStanza in which Stanza GC is written.

Interestingly, D language pioneered this combination both GC (by default) and non-GC more seamlessly, even before Stanza.

In addition to Ruby, these four languages namely Elixir, Groovy, Stanza and D all have similar to or better expressive power than Ruby. Notably both Stanza and D are compiled languages. Above all D is an anomaly in a good way since it's a fully type programming language. Kudos to Walter and the team for giving birth to a highly expressive fully typed modern language, very fast in compilation and runtime, truly one of a kind [3].

Regarding the issue of comparatively smaller corpus for these languages as mentioned by others, I think the new self-distillation technique for LLM and code generation as proposed by Apple, MIT-ETH and UCLA can overcome this limitation [4].

[1] “Stop Designing Languages. Write Libraries Instead” (2016) (278 comments):

https://news.ycombinator.com/item?id=46525640

[2] Stanza: People:

https://lbstanza.org/people.html

[3] Origins of the D programming language:

https://dl.acm.org/doi/10.1145/3386323

[4] Embarrassingly simple self-distillation improves code generation (201 comments):

https://news.ycombinator.com/item?id=47637757

> 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)

I am actually writing a paper on this right now so nothing I can point you to yet but yes. LLMs are better (produce working code in fewer attempts controlling for the relative size of training corpus) when using type systems with inference and global unification. It is largely about the quality of the error feedback channel so languages with very good compiler errors (accurate, localized, include the correction with the failure) can close a lot of ground.

But inference + sound type system gives you a constraint propagation that genuinely restricts the ability of the LLM to get into trouble. Type systems that require annotation give up most of the benefit, since the annotations are themselves surface area for LLM mistakes. Unification also puts heavy limits on the expressiveness of the language which is a confounder and may actually be a big part of the benefit too.

Everyone has been on the "the training data is better" thing but I actually don't think so. All of the languages that people report as being better because of good training data actually have fairly restrictive type systems. Elixir is an exception, but it has exceptionally good error messages! And also, along with erlang, pretty unique runtime semantics that may contribute but that's outside my domain I'm on type systems. Debunking the training quality thing is not what I'm working on but I have deep suspicions about that common wisdom.

One thing something like AutoCodeBenchmark cannot demonstrate is what happens when you have human-written type definitions defining the domain before the LLM writes a line of code.

That is something I have found very effective in F#, that I model the domain with types, I know what the type signatures of the functions I need are, and the LLM does the work of actually implementing those functions.

Here is a concrete example:

I have been playing around with a program to assist me with projects I make at home on my hobby-grade CNC router, which does not have an automatic toolchanger. I use a mix of Vectric VCarve and some older handwritten programs to generate GCode files. I end up with a USB drive with maybe 6 to 12 GCode files on it and a model in my head of "to make this product, I start with a board here, gotta install this square nose end mill and zero on this corner of the board, run files A and B. Then install a ball nose end mill and run file C. Then flip the board over lengthwise, switch to a smaller square nose end mill, zero here, run file D. etc. etc."

Although I try to name the GCode files in a self documenting way like 01_TopSide_25square.ngc, if I come back in 1 year and want to make the same thing again, I pretty much always have to open VCarve and eyeball what the hell all the files did and confirm where to zero, what size board to use, etc. So I'm making a tool where I can define those human-operator steps that go with the G-Code files, save it as a "project file", preview in 3d what each step will look like, and export to a printable PDF with screenshots and step-by-step instructions. Hopefully this will reduce the amount of rot that these projects suffer and the cognitive overhead of picking up an old one.

Modeling the steps as F# types was the very first step, like (small excerpt):

    type WorkpiecePlacement =
        {   Id : WorkpieceId
            /// Corner of the workpiece we'll attach to the machine.
            WorkpieceCorner : WorkpieceSpace.Corner3D
            /// Point in machine-space we'll anchor this corner to.
            MachinePoint : MachineSpace.Point
            /// Which face of the workpiece is on top.
            FaceUp : WorkpieceSpace.Face
            /// Rotation around the up-axis.
            Yaw : WorkpieceSpace.Yaw
        }

    type OperationType =
        | PlaceWorkpiece of placement : Operation.WorkpiecePlacement
        | InstallTool of id : ToolId * slot : int option
        | ZeroAt of point : MachineSpace.Point
        | RunGCode of source : GCode.Source
        | RemoveWorkpiece of id : WorkpieceId

For the GCode simulator I needed a parser for GCode files, which produces a type with 1:1 equivalence to the GCode instruction set:

    type GCodeInstruction =
        // --- Motion ---
        | G0_RapidMove of axisMoves : (Axis * float<gcodeunit>) array
        | G1_Move of feedRate : float<gcodeunit/minute> option * axisMoves : (Axis * float<gcodeunit>) array
        | G2_ClockwiseArc of ArcParams
        | G3_CounterClockwiseArc of ArcParams
        | G4_Dwell of seconds : double

        // --- Plane selection ---
        | G17_SelectXYPlane
        | G18_SelectXZPlane
        | G19_SelectYZPlane

        // --- Unit selection ---
        | G20_Inches
        | G21_Millimeters

        // --- Distance mode ---
        | G90_AbsoluteDistance
        | G91_RelativeDistance
        // ... etc truncated, more instructions in real code

But my tool supports doing transforms on toolpaths, like rotating 90 degrees or offsetting so I can easily define that I want to make tiling copies of the same project. To implement those transforms straight up as GCodeInstruction[] -> GCodeInstruction[] is a bad call. GCode is very stateful and lets you switch units, relative vs. absolute coordinate spaces, etc. in instructions. That makes the transform awkward and tricky to write.

So I have a ToolPath type that makes the transforms clean. It normalizes the many ways of expressing the same toolpath in GCode to a single representation with all absolute coordinates in metric units.

    type ToolPathInstruction =
        | Rapid of From : Point * To : Point
        | Linear of From : Point * To : Point * Feed : FeedRate
        | Arc of
            From : Point *
            To : Point *
            Center : Point *
            Plane : Plane *
            Direction : ArcDirection *
            Feed : FeedRate
        | ... etc truncated

That is the appropriate level for the transforms like offset, rotate, scale, etc. to operate on.

Yet there is still ANOTHER level of toolpath-related operations that deserves its own type. When I'm doing simulation of material removal to check for crashes, or rendering the toolpath in 3d, I don't want to deal with arcs! The rendering/simulation is inherently an approximation. It will break down each arc into line segments. So sim code and rendering code shouldn't take a toolpath, it should take basically a line segment list, or in other words...

    type ApproxMove =
        {   From : Vector3
            To : Vector3
            FeedRate : double<m/minute>
            IsRapid : bool
        }

    type ToolPathApproximation =
        {   StartPosition : Vector3
            Moves : ApproxMove[]
        }

Having defined all these types it's clear that I need operations like:

    parse: string -> GCode
    serialize : GCode -> string
    normalizeToToolPath : GCode -> ToolPath
    denormalizeToGCode : ToolPath -> GCode
    offset : Vector3 -> ToolPath -> ToolPath
    rotate90 : ToolPath -> ToolPath
    scale : Vector3 -> ToolPath -> ToolPath
    approximate : ToolPath -> ToolPathApproximation
    simulate : ToolPathApproximation -> MachineState -> MachineState
    renderToolPathWireframe : ToolPathApproximation -> VBO
    renderMachineState : MachineState -> VBO

And so on. An LLM is absolutely awesome at one-shotting the implementations.

I would find it quite frustrating trying to model the same domain without any types, either having all methods working on a single toolpathy data structure that's not really the right fit for any of the places it's used, or having them work on multiple data structures without any clear delineation of which layer is expecting which toolpathy-thing that are all subtly but importantly different.

> It’s pretty rare that I run into a bug in production that a type system would have caught.

Wow, how different our experiences are. In Javascript/Typescript land, so so many bugs are null/undefined-related and really should have been caught at type level.

In fact, I'd say (without actually measuring it) that _most_ bugs I've ran into in Typescript are due to someone having bypassed the typing (casting, ts-ignore...), or a type mismatch at IO boundary.

Go is pretty great - here's a list of tools I use to help me write/build Go- maybe a few of them will also be what you need: https://www.bbkane.com/blog/go-project-notes/

> It’s pretty rare that I run into a bug in production that a type system would have caught.

Well yes, surely because you’re not designing your system around the type system. You need to architect your project to lean heavily on types, pattern matching, etc to actually gain the benefits. If you move a JS project to TS and just rename the files, yeah there’s going to be no difference, you must reengineer the entire codebase to leverage the type system.

Personally, after moving to TS I’ve been completely sold on types and am currently planning to migrate my app to F# so I can gain even more benefit.

C is among the most token efficient languages out there and is statically typed.

Typescript is very verbose thus it cannot compete with much denser languages on token efficiency.

By the way, the biggest reason many love statically typed languages, especially those that are quite expressive like TypeScript is for the domain and data modelling. Makes it easier to reason about the program and to refactor.

I tried doing my side projects in Go and one thing I miss is the rails console which is so helpful. I guess I could have it write a go console or something but it’s not quite the same

> to more performant runtimes and architectures in response to operational concerns at scale, which have a tenuous link to language

The runtime performance and the language are deeply linked. None of the dynamically typed runtimes you mention are actually performance competitive with JVM languages.

> Not necessarily. Since the word "typed" language is not well-defined.

This depends entirely on context. In the Benjamin C. Pierce school of thought (a common choice in programming langauges research; see his book Types and Programming Languages, 2002), "typed" means what we typically call statically typed, i.e., the language employs a static analysis to prevent the compilation/execution of (some subset of) faulty programs. Meanwhile, languages that are commonly called "dynamically typed" are, in this school of thought, not typed (or "untyped"). (TAPL provides a more rigorous definition, but it's in the other room and I am lazy.)

As I understand it TypeScript does not enforce types at runtime. Am I correct? If so that would signify to me it is not a "typed language", like say Java for instance. Types in TypeScript are more like "annotations" for docujmenting the program. Am I correct?

Rather than having the LLM and human devs all guessing from verbose variable names, can't they both use a language server that observes the code and can surface that kind of structure info cheaply?

Part of the point of types is enforcing more of the contract at various code boundaries (function, module, etc), and that enforcement is specifically so that you don't have to keep the whole codebase in your head / context window in order to be able to work on it.

> the errors I get at runtime are almost never type-based

That surprises me, but everyone's experiences are different. I've been in the statically typed language space for so long and enjoyed it so much, I find it pretty irritating to go back to Python (my long-ago favorite) but many people are in the exact opposite frame of mind. I'm curious: what kinds of errors do you classify as a type-based error? I think that varies from person to person.

For example, null references. A C programmer would say dereferencing a null is not a type-based error, because it's not feasible to encode non-nullable pointers in the C type system. A Haskell programmer would say it is a type-based error because Haskell makes it difficult not to encode this in the type system, you really have to go out of your way to create a runtime null dereference error.

A C# or TypeScript programmer could answer differently depending on who you ask, because both of those languages make it possible to leverage the typechecker to prevent null-deref at compile time, but neither one makes it required (you can turn those checks off or make them warnings if you like), so it depends on the programmer's build settings and how much typechecking they personally have chosen to use.

This reminds me of the analogy of the smoking grandpa. I had a grandpa that was chainsmoking his whole life and managed to reach 90 and died of other causes. This does not mean smoking is "relatively safe".

I've been working with typescript for the past ten or so years.

A couple of years ago I did some contract work for a client who used Javascript.

I did some basic smoke testing to understand the state of the app and I was able to get lots of fun type errors on the server and client at runtime just by QAing the damn thing.

I've definitely found LLM code to be syntactically/semantically correct in one-shot pretty much all the time. It's usually the functional specification/behaviour that's found wanting.

Typing probably makes sense where memory-correctness needs to be enforced (e.g. Rust), and inferring those semantics require a much wider context. But memory-correctness isn't really something that afflicts BEAM languages.

when i was programming elixir by hand i was making typing errors about 1 every half year or so. none took production down, most were caught and corrected quickly from logs. now im doing mostly llm elixir, almost all typing errors are caught in integration tests and only one has made it to prod.

I thought a big part of the reason for type systems was a sort of self documentation/contract? Especially if you need to work on an unfamiliar system with bad documentation. Also what about system boundaries? I prefer typed languages personally.

Types always have to be checked. Either at compile time or at runtime. And if you're weakly typed you still check them to see if you use normal or backup behaviour.

If you're statically typed you can remove the actual check from the binary. They are therefore also a performance thing.

Types are useful for squeezing more performance.

Having been at a several places that have gone from framework-makes-us-fast to too-massive-for-the-framework, engineering velocity works as a function of how much mental context is needed and how many people/teams have to collaborate.

As orgs grow, the only way to maintain velocity is to reduce mental context. Humans have to reason about their systems.

In the half a dozen engineering orgs I have worked, each and every one became a quagmire of slow eng velocity and saw increased velocity and less bugs as they reduced context needed by teams. Separation of concerns, allowing individual services that run independently, more and better tests and observability, and, yes, better typing.

Lots buy into the view "the old system got us here and now we can afford to rewrite and do things 'right'." The real cost is, literally, moths to years of dev efforts to unwind tangled concerns. Million to tens of millions in developer salaries that are going towards keeping the ship afloat as the hull is changed out. The opportunity cost is truly mind blowing.

To avoid that cost: keep concerns separate, define data domains, and use a language that allows you to keep logic localized. If you have to jump files to understand your incoming parameters, you're gonna have a bad time when things no longer fit in your head, and esp. when new to the code as a new hire.

Elixir, I still had to know my whole call chain to know what I could do with my incoming parameters. The more call sites, the more mental context. I choose static types because I can KNOW what my function is receiving locally: it is the type signature.

I would like to validate my experience against other static typed languages like c#; so far, I have seen wins at every org that switched from dynamic languages to Go. Go seems to get a lot right for helping eng orgs move faster.

> Typing generally slows down languages, not speed them up because of all the additional checks that must be done.

Source? You seem to be talking about compile-time versus runtime, and I've not even heard of compile times being significantly slowed by type checking.

> The dynamic stuff is part of what slows down languages like Python and makes them tricky to optimize.

That seems to harm rather than help your previous claim. In untyped languages, in principle every object has to be treated as dynamic.

Yeah we’ll see how that goes when the VC subsidies run dry and everybody gets corralled into token-based pricing.

I use rails because it makes thousands of good choices that I never have to make. If build apps the rails way I don't have to deal with a mountain of tech debt (in the form bad or ever changing choices).

What lower level lang would offer the benefits the beam/otp provide? I suspect you're generalizing a bit too much and haven't thought this through :)

So the future of programming is asking an LLM to spit out the appropriate assembly?

What will you use as training data for these new languages?

LLMs are good at current programming languages because they had lots of data to train on.

theres nothing in common between humans and llms or llm training sets!

I’m so happy with switching all my dev over to rust since AI coding. Everyone is lighting fast and super reliable