In an age of AI, is static typing even necessary?

Wikis, Polls & Dev Envs Polls
, , ,
21

I am already seeing that AI agents will produce a solution with a typing violation (in Typescript) and correct themselves on the fly. I am certain when Elixir types land, the same will happen with Elixir.

Imagine you optimize for a new engineer is joining your project and they need to get productive quickly. Whether that new engineer is an AI or a human being will is almost irrelevant. Because it’s a very similar thought process:

  • Documentation helps
  • Comments help
  • Consistent project structure help
  • Being concise is better than being too verbose
  • Types will reduce the chance they structurally break things

I think it might matter because sometimes us humans might still need to pop open the hood to inspect what’s going on. It might also matter for the AI itself. After all, the AI will need some sort of representation of the code that’s easy for the AI to work with. And i think that higher level representations are probably more efficient.

For arguments sake imagine AIs had to write assembly code instead of JS. It would be a lot harder for even the AI to produce working code. Again the point is that the code representation will still be very important for AIs. Perhaps languages will need to evolve to be easily digestible for humans AND AI, but it seems to me there is a lot overlap.

3 Likes
22

Totally, the point I was making was only that, for a type system, you have to validate the keys in order to “type” the map. If you don’t validate the keys the type system can’t guarantee they’re there, so you’re back to square one.

With that said, another case occurred to me: partial validation. If you wanted to guarantee that a struct has, say, %{"id" => String.t} but allow any other fields, mixing atom keys and string keys would be pretty gross. I think that’s a pretty good argument for string literal types, actually. Consider making a thread about it!

2 Likes
23

AI needs to be explainable first, or mishaps could end up being buried too deep.

My humble opinion.

SVM powered typing perhaps?

2 Likes
24

I hope this doesn’t come off as too far off-base to your question - but it got me thinking about language (both natural and context-free).

All languages have tools its users use to signify different qualities of meaning. They’re just tools - sometimes they’re right for the job, sometimes they aren’t.

For example, a non-native English speaker might dislike having to always include an article (a/the) if they come from a language that doesn’t bother. (a cat, the cat, why are you forcing me to care?)

Likewise, English speakers might have trouble with other language systems that use grammatical gender. (why is it la mano, again?)

I think of types in a similar way, AI or not, they can be very useful if they’re the right tools for the job.

1 Like
25

Well, verification is possible with types being first class citizens (dependent types,) and there is Idris for that (which is Haskell done right,) save for that it unfortunately cannot reach the production stage (due to very few people working on it.) I personally design complicated solutions in Idris first, prove the stuff, and then translate to Elixir (losing the proof, I know, but hey, I am a good translator :).

Also, there are some languages to explicitly make proofs, like Lean, Coq, Agda—this one is too esoteric even for me—etc.

But ADTs without dependent types, with types not being first class citizen, seems to be like AST, built on top of the regex-parser of the compiled code. I know this opinion is not popular, but I truly see no reason in having type checks when I cannot make types to depend on my other code and vice versa. I don’t fear to pass %User{} to where %Product{} is expected and never notice it until this bug crashes prod.

4 Likes
26

I do agree but with stuff like Dialyzer and the more and more improving Elixir compiler on the scene I’d say that being 20% - 30% there is still better than being 0% there.

And any tool that can help ground the LLM and give it a feedback loop with which it can self-correct, is a net gain.

4 Likes
27

I honestly dunno. That sounds perfectly legit and it still bugs me to my gut. If I were able to figure out what type is there—LLM surely could have it done too. If it could not—it means I have a flaky design which wouldn’t be much improved by restricting types flowing around.

I wrote many AST-like parsers in my life and I’ll tell you what. There are two approaches to accomplish such a task. The one is to explicitly specify the expected income and isomorphically move it into the matching clauses (in the wild assumption you have a comprehensive spec on hand and it’s flattenable to clauses.) Another one would be to start with a single clause, printing the income and raising straight away. That way you got your first matching clause (and the second one which still raises.) In a dozen (hundred) iterations you are all set, and you have your parser on hand. I expect the LLM to act that way. Like, saying “Hey, man, the changes in this commit added new value passing to this function ("admin") which is extra to previously handled "user" and "guest".”

2 Likes
28

As humans we often call a function based off of documentation without reading the implementation. The models are likewise generally unable to fit the full codebase of all dependencies in context (often they can’t even fit your codebase in context) and so as it turns out documentation which does fit in context is very helpful to them. The recent Ash AI efforts and what Zach has written about them indicates, to me, that documentation is very important for the models to perform today.

And personally, when writing Elixir the typespecs are the first thing I read on hexdocs when I’m looking up a function. So clearly they are a very useful form of documentation. A type checker is helpful because it checks that those typespecs are actually correct, which catches bugs in the documentation.

Agreed.

4 Likes
29

In a true age of AI, we won’t have the computer writing Elixir or Java or even C or assembly, but instead skipping all the abstraction overhead that was created to make it easier for humans to write code (correct or otherwise) and skipping straight to machine code. OK, maybe there is a terse sort of machine code-like abstraction to achieve portability. But the point stands: the AI becomes the abstraction and shouldn’t need intermediate abstraction layers to be successful. In some sense “static typing” continues to be important because at the lowest level you are allocating some part of computer memory to hold a value of a particular size or to hold a subroutine and you need to know where that starts and ends to access it and use the rest of the memory efficiently, but that’s not static typing as an abstraction which I think is what the poll question is aiming at.

Until that time, LLM coding is about machine/human cooperation in programming which needs to accommodate the human side to be effective. Therefore, if static typing helps humans write more robust code the need for static typing won’t change just because an LLM is in the loop. Arguably it becomes more important because, as others have pointed out, it becomes the most explicit expression of intent between human and computer (just as it does between human and human).

4 Likes
30

Interesting, ive tried idris because of the type driven development with idris book, I dropped it because I just did not have the motivation/time to get up to speed with emacs, getting idris2 mode to work properly with vscode felt like a nightmare and also I just didnt get the immediate benefits of writing programs in it like I did with phx, bar the code being succinct.

but now I am interested in your work flow, how do you design programs in idris before you write them in elixir. What sort of benefit does such exercise grant you?

2 Likes
31

Ya, this is the far more likely case, but I was imagining the future where no one looks at code or even knows how to read it. Which is of course a bit ridiculous—obviously there are people who still write in assembly. And in that case then @sbuttgereit’s point that AI would then just be the abstraction makes far more sense.

I did vote that static types will still be useful (even though I don’t love using them myself).

2 Likes
32

Idris brings proofs. It assures me I chose the correct approach and implemented it properly. Well, the evident example from the latest week: I was after the cumbersome throttling with retries and I have proved the functions are total and the code never increases the number of retries beyond the limit. Idris would not compile the code if the dependent (on number of retries in this particular case) type goes upper limit (or below zero.)

Another example would be a finite automata implementation, where Idris validates during a compile time, that e. g. in the state “paid” say the amount of money had decreased and the receipt had been issued.

1 Like
33

I am not so sure. What Zach has written is a normal scepticism about the hipe, but I have not read it as “more docs would give LLM more context.”

Speaking from my own experience, LLMs today are extremely, unbelievably great at writing documentation. I mean, once I have a clean code, LLM would have a documentation produced that would be 100 times better than what I can do myself.

That I could not agree more, but it’s kinda irrelevant to the topic. I like drinking barrels of coffee during hard coding sessions, but it does not mean LLM would like it too.

2 Likes
34

I gave it another thought and I can tell that in my opinion, what would actually improve an LLM code-execute-fix loop drastically, would be generous error messages, being an actual guideline whenever possible, like in Rust:

help: consider cloning the value if the performance cost is acceptable
    |
269 |             layers: vec![layer_digest.clone()],
    |                                      ++++++++

Some errors have detailed explanations: E0382, E0428.
For more information about an error, try `rustc --explain E0382`.
1 Like
35

Ah right it’s an interesting thought experiment!

Don’t you feel that even if the code is only for the AI, it would still be more efficient for an AI to have higher level languages–not so different from what humans use?

I’d imagine that, even if a programming language was JUST for an AI, high level programming languages would be easier for the AI to reason about and faster to produce. I can’t imagine a benefit for an AI to work with low level coding languages even if humans aren’t involved.

36

I believe @sbuttgereit touched on this here:

But honestly I can’t contribute any deeper than speculation on this topic since I have only read a mere handful of words describing at a very high level how LLMs work.

37

I had asked him about it on here and he indicated that providing clear documentation on how to write Elixir and Ash were very helpful for improving the model outputs, and I believe he’s now spearheading an effort to get more libraries to add that sort of “condensed” documentation.

To be clear, “context” in my post was a technical term, i.e. the transformer “context window”. In other words, it’s important to include clear instructions within the prompt. Agents are able to “search” through the codebase by various means, including RAG, but this is much less effective than actually having things in context. But the context window is only so large, so you can fit a lot more typespecs than actual code, was my point :slight_smile:

Of course that point was predicated on the preceding argument: docs are good for models, typespecs are good docs (for me), therefore I suspect typespecs are good docs for models.

This is actually a very interesting point. If you think about it, what you’re actually doing is pre-computing the model’s understanding of the code and condensing it down so that it can fit into the context of another prompt. It’s similar to RAG, except you are condensing the output into tokens and running it straight through the model.

Some of the latest LLMs are actually doing KV compression natively within the model (compressing the KV cache into a latent vector). It’s all related, I think.

3 Likes
38

I voted other because I don’t care about static typing but I care about ‘strict typing’, and especially type hinting function parameters. It’s a real drag on my productivity with elixir. And no, writing @spec is not up to 2025 standards.

39

Static typing or not. Most bugs are logical.

3 Likes
40

Interesting discussions. One aspect in predictions about widespread agentic ai adoption that often gets overlooked is trustworthiness.

In my opinion, there is a possibility within the next 5 years code generation quality, safeguards, agentic ai SDLC loops, and so on could improve to such an extent that risk of introduced vulnerabilities is not significantly greater than average human software development.

But the crux of the matter is, how much would you (would anyone) ever trust AI to fully develop & run software critical for business operations over human developers? And what sort of proof is actually going to convince your average business leader? (My guess, it would require widespread adoption with very few ai-introduced vulnerabilities, so it’s a catch-22). Throw in things like potential job loss, unionization, legalities (was the data LLMs were trained on really permissible?), politics, etc. and the way forward is very bumpy.

After the whole world’s exposure to LLM hallucinations, its trustworthiness is already severely compromised and, despite the very loud AI evangelists, trepidation about it is at an all-time high. Despite many businesses’ FOMO and rush to experiment with it, it’s only going to take one publicized vulnerability introduced by AI to set back agentic software development back years.

With that in mind, I think any current software best practices like static typing (whether you think static typing is a best practice is debatable of course!) and other high-level abstractions of all kind, including non-machine-code languages, are crucial for human verification, which I don’t foresee going away any time soon.

A humanistic ai-enhanced software development process (such as Spec-then-Code*) is the infinitely saner, less apocalyptic way forward for now for all human parties involved. My $0.02 anyway.

GitHub - mosofsky/spec-then-code: LLM prompts for structured software development because quality takes more than just "good vibes".
From “Vibe Coding” to “Vibe Software Engineering”

4 Likes