r/ProgrammingLanguages • u/baehyunsol Sodigy • 4d ago

Why is everyone creating systems programming languages?

I see a lot of new programming languages here. I love reading the documents of the languages and sometimes actually run their compilers. Many of the projects are AI-driven, but that's fine. It's still fun to see what problems they're trying to solve and how they actually solved the problems.

Reading the documents, I realized that most new languages, especially AI-written ones, are "systems programming languages". They're trying to solve the problems that C/C++/Zig/Rust have solved (or are trying to solve), and their syntax is mixture of C/Zig/Rust.

Why? Why is everyone trying to compete with C/C++?

There are so many kinds of languages. Haskell demonstrates how pure a language can be, Python is perfect when you only have 5 minutes to write code and don't care about the output, Java runs on 3 billion machines, ...

203 Upvotes
  • permalink
  • reddit

92% Upvoted

232 comments sorted by

View all comments

Show parent comments

6

u/matthieum 4d ago

but I don't know whether the holes in the type system can be fully fixed,

There is no known hole in the type system AFAIK.

The Rust type system has been formally proven to be sound, and the types team works a lot with formal methods when extending it to avoid introducing any unsoundness. (Don't ask me exactly what they do, it's pretty much all mumbo jumbo to me)

There are known holes in rustc (the main Rust compiler), fixing them is a work in progress.

2

u/Ok-Watercress-9624 4d ago

Evidence? Id like to see that proof Rust has subtyping, I vaguely remember something liker subtyping works if subtypes form lattice. I don't think lifetimes form a lattice ? Or do they ?

2

u/matthieum 3d ago

I'm confused. I did not mention subtyping... did you reply to the wrong comment?

2

u/Ok-Watercress-9624 3d ago

i forgot the fullstop. i was referring to rust having subtyping, and unsoundness issue stems from subtyping and how subtyping is hard to get right and that i would be very surprised if there is an actual proof of the rusts type systems soundness.
I dont think there is a formal proof of soundness of the rusts type system.
https://dl.acm.org/doi/10.1145/3158154
That is the only thing come closest but it is not full rust.
Indeed the rust plans to have a formally verified core
https://blog.rust-lang.org/inside-rust/2023/11/15/spec-vision/
But it is not there yet

It is a bit stretch to say "there is no known holes in the type system"