We used methods akin to this back in 2019 for creating low-level HALs for insanely complicated SoCs (think experimental switch fabric controllers). We wanted the compiler to reject any program that was attempting to access the hardware incorrectly because the dev-test cycle was slow, the hardware was very fiddly, and debugging was miserable. The register definitions were all generated from the supplier data sheet (a clojure program we wrote parsed a PDF then emitted Rust).

We wrote a blog post about the Rust type-level programming part of the approach: https://blog.auxon.io/2019/10/25/type-level-registers/

Before const generics, you needed this kind of "types" to use integer values in generics, for example for fixed-length vectors/matrices/... (and const generics still have limitations).

https://doc.rust-lang.org/reference/items/generics.html#cons...

They came with 1.51: https://blog.rust-lang.org/2021/03/25/Rust-1.51.0.html

This technique is good for job interviews, when they ask me to solve leetcode problems. I was inspired by the blog:

https://aphyr.com/posts/342-typing-the-technical-interview

and related to Rust, the solution

https://github.com/insou22/typing-the-technical-interview-ru...

Or Typescript https://www.richard-towers.com/2023/03/11/typescripting-the-...

As others mentioned, nowadays const generics replace this technique for most problems. This technique however is still useful if you need something like `[T; A+B]` (an array whose length is the sum of two generic constants), which is not yet possible with const generics.

Not really in the programming mainstream, but in research-oriented languages with dependent typing like Lean or Idris, constraining your "implementation search space" with types and leveraging the type system to prove properties about your program is commonplace.

While not nearly as involved, I've seen similar-ish techniques used for FFTs and similar algorithms, in order to precompute constants.

Here[1] is an example in C++ but given the article it seems you could do something similar in Rust.

[1]: https://github.com/tmolteno/template-fft/blob/master/fft_rea...

Theres a train company using these to prove the microcontrollers and train network cant be in bad states. check youtube

Something like a typed heterogeneous list is often build in a similar way.

A simpler version is probably a simple non empty list where you always have the guaranty of at least one element.

Theorem provers that use dependent typing, like Coq.

Life critical mathematics: you could verify calculations in the type system which are too risky to allow to fail at runtime.