While I don’t know if this approach will work, I find it very refreshing how laser-focused José seems to be on “the type-system is there to prevent bugs”. It’s a welcome change from other programming languages where I get the feeling the type system is mostly developed so that people can write papers about it.
other programming languages where I get the feeling the type system is mostly developed so that people can write papers about it
As an academic working on type systems, I find this anti-academic comment borderline offensive. It’s a massive amount of work to implement type systems for real-world programming languages, and there are many easier ways to write papers. People develop type systems because they want to help / improve a language they care about – somewhat more rarely, because they are paid to do it.
I don’t think the comment was anti-academic. It points out that some languages go overboard with the over-engineering of their type system. Some, not all.
It does not critic the work most academics do, which, as you said, aim to improve the state of the art.
You point does not negate the parent; the fact is, scvalex’s comment is too vague to extract a concrete criticism, but it certainly conveys dismissal of academic contributions to type theory. This is a very familiar anti-intellectual tone of “ivory-tower elite” vs “practical working programmers”, let’s not pretend that this isn’t commonplace in the industry.
I didn’t mean the comment as a dismissal of academic contributions. I meant it as a complaint about priorities. There’s a time and place for everything and as a user of languages, I’d rather have features that make programming nicer now instead of waiting for a research project to complete. I think the research project should still happen, but in some way that doesn’t block adding useful features to the language (e.g. a fork of the language or a custom language).
Mind you, the Elixir work here is actually a research project. But it’s clearly focused on solving real day-to-day issues rather than just developing set-theoretic types in the abstract. And, as they’re figuring things out, they’re adding them to the language making it better. I like this approach and I’d like to see more of it.
I do concede that my comment above was too vague, but I didn’t want to bring up a different programing language in a post about Elixir’s type system. I probably should’ve refrained from commenting and written up my complaint as a separate post.
For context, see José Valim’s talk on the design of Elixir’s type system at ElixirConf 2023:
https://www.youtube.com/watch?v=giYbq4HmfGA
While I don’t know if this approach will work, I find it very refreshing how laser-focused José seems to be on “the type-system is there to prevent bugs”. It’s a welcome change from other programming languages where I get the feeling the type system is mostly developed so that people can write papers about it.
As an academic working on type systems, I find this anti-academic comment borderline offensive. It’s a massive amount of work to implement type systems for real-world programming languages, and there are many easier ways to write papers. People develop type systems because they want to help / improve a language they care about – somewhat more rarely, because they are paid to do it.
I don’t think the comment was anti-academic. It points out that some languages go overboard with the over-engineering of their type system. Some, not all.
It does not critic the work most academics do, which, as you said, aim to improve the state of the art.
You point does not negate the parent; the fact is, scvalex’s comment is too vague to extract a concrete criticism, but it certainly conveys dismissal of academic contributions to type theory. This is a very familiar anti-intellectual tone of “ivory-tower elite” vs “practical working programmers”, let’s not pretend that this isn’t commonplace in the industry.
I didn’t mean the comment as a dismissal of academic contributions. I meant it as a complaint about priorities. There’s a time and place for everything and as a user of languages, I’d rather have features that make programming nicer now instead of waiting for a research project to complete. I think the research project should still happen, but in some way that doesn’t block adding useful features to the language (e.g. a fork of the language or a custom language).
Mind you, the Elixir work here is actually a research project. But it’s clearly focused on solving real day-to-day issues rather than just developing set-theoretic types in the abstract. And, as they’re figuring things out, they’re adding them to the language making it better. I like this approach and I’d like to see more of it.
I do concede that my comment above was too vague, but I didn’t want to bring up a different programing language in a post about Elixir’s type system. I probably should’ve refrained from commenting and written up my complaint as a separate post.
You realize that the most common reason people develop new type systems and write papers about them is to prevent bugs?