Right, only you don't know what it's called, where to download it, or how to write the code.

Why? I do. Search for dependent types.

https://github.com/FStarLang/FStar

Calling your bluff; you've never used this.

>only you don't know what it's called, where to download it, or how to write the code.

>you've never used this.

What next? You've asked for an example of powerful typesystem, here, you got it. Other examples are SPARK, Coq, Liquid Haskell, Idris, C++20, Agda.