Interestingly, the Lean theorem prover is sometimes considered a bit of a mess type-theoretically. (an illustrative thread), but is perhaps the most popular theorem prover among mathematicians. I would say it’s more on the “maximalist” side.
Last I read about Rust’s type system, it basically didn’t have a theoretical basis, and seemed like it was just based around Graydon figuring out algorithms for getting the properties he wanted. Rust is much more popular than SML (or Haskell, though I’m not sure Haskell should really count as a ‘minimalist’ type system with all of its language extensions).
Interestingly, the Lean theorem prover is sometimes considered a bit of a mess type-theoretically. (an illustrative thread), but is perhaps the most popular theorem prover among mathematicians. I would say it’s more on the “maximalist” side.
Didn’t know this about Lean, but the fact that a maximalist option is most popular with mathematicians makes sense to me. As someone who worked both with mathematicians and formal methods researchers (much more meta-mathematicians), the latter are much closer to programmers, in the sense that they want to build things and solve their own abstract problems, instead of necessarily wanting the most compositional machinery possible (although I still expect compositionality to be baked into the intuitions of many mathematicians).
Last I read about Rust’s type system, it basically didn’t have a theoretical basis, and seemed like it was just based around Graydon figuring out algorithms for getting the properties he wanted. Rust is much more popular than SML (or Haskell, though I’m not sure Haskell should really count as a ‘minimalist’ type system with all of its language extensions).
Rust is an interesting point in the design space. If I had to describe it quickly according to the framing above, it feels like a really pleasant fractal tradeoff between different type systems:
It has an ML type system with algebraic datatypes (and even traits which are close to typeclasses in Haskell)
So it definitely feels more maximalist than some ML or some pure linear type system, but that’s more from the combination and UX work than from a crazy “let’s add this super advanced feature” rush à la TypeScript imo.
Interestingly, the Lean theorem prover is sometimes considered a bit of a mess type-theoretically. (an illustrative thread), but is perhaps the most popular theorem prover among mathematicians. I would say it’s more on the “maximalist” side.
Last I read about Rust’s type system, it basically didn’t have a theoretical basis, and seemed like it was just based around Graydon figuring out algorithms for getting the properties he wanted. Rust is much more popular than SML (or Haskell, though I’m not sure Haskell should really count as a ‘minimalist’ type system with all of its language extensions).
Didn’t know this about Lean, but the fact that a maximalist option is most popular with mathematicians makes sense to me. As someone who worked both with mathematicians and formal methods researchers (much more meta-mathematicians), the latter are much closer to programmers, in the sense that they want to build things and solve their own abstract problems, instead of necessarily wanting the most compositional machinery possible (although I still expect compositionality to be baked into the intuitions of many mathematicians).
Rust is an interesting point in the design space. If I had to describe it quickly according to the framing above, it feels like a really pleasant fractal tradeoff between different type systems:
It has basically affine type but with more practical usage through borrowing (see this survey for more details)
It has an ML type system with algebraic datatypes (and even traits which are close to typeclasses in Haskell)
So it definitely feels more maximalist than some ML or some pure linear type system, but that’s more from the combination and UX work than from a crazy “let’s add this super advanced feature” rush à la TypeScript imo.