> But why have a separate type system instead of just building it into the language.
Excellent question. The existing "mainstream" languages (C++, Rust, Julia, or even Haskell) are not designed to support such applications as bound checks or pointer checks in their type systems, where certain runtime values/checks can affect/refine the types (as in dependent types, or refinement types which Liquid Types are based on).
It could be done (in some newer languages: Idris, Agda, Lean), but people have not figured out an ergonomic way to do so in more "mainstream" languages (e.g., not hurting type inference, light and maintainable proof burdens). Liquid Haskell is an attempt to bring refinement type to Haskell, as an extrinsic type system.
> C++ could build in pointer checks and it would be in the same type system.
People have not figured out how to do so (and I doubt if it is possible at all). Suffice to say:
* Rust is an attempt to build in lifetime-and-ownership-checks into the type system of C++, and Rust is a new language,
* Liquid Rust is an attempt to add pointer checks (refinement types) to Rust, and even then it is not built into Rust.
> And with _this_ rebuttal, the issue is now double settled.
People are still researching solutions (see Rust and Liquid Rust over C++) to this problem (building in pointer checks in the type system of C++), and they would love it if you can settle their problems.
Excellent question. The existing "mainstream" languages (C++, Rust, Julia, or even Haskell) are not designed to support such applications as bound checks or pointer checks in their type systems, where certain runtime values/checks can affect/refine the types (as in dependent types, or refinement types which Liquid Types are based on).
It could be done (in some newer languages: Idris, Agda, Lean), but people have not figured out an ergonomic way to do so in more "mainstream" languages (e.g., not hurting type inference, light and maintainable proof burdens). Liquid Haskell is an attempt to bring refinement type to Haskell, as an extrinsic type system.
> C++ could build in pointer checks and it would be in the same type system.
People have not figured out how to do so (and I doubt if it is possible at all). Suffice to say:
* Rust is an attempt to build in lifetime-and-ownership-checks into the type system of C++, and Rust is a new language,
* Liquid Rust is an attempt to add pointer checks (refinement types) to Rust, and even then it is not built into Rust.
> And with _this_ rebuttal, the issue is now double settled.
People are still researching solutions (see Rust and Liquid Rust over C++) to this problem (building in pointer checks in the type system of C++), and they would love it if you can settle their problems.