No too my knowledge nothing is strict about a proofing system because like I said it becomes hard to do. It could be useful for ultra safe software but for most cases the complexity isn't worth it.

But that doesn't mean it's not useful to have this capability as part of your typesystem. It just doesn't need to be fully utilized.

You don't need to program a type that proves everything correct. You can program and make sure aspects of the program are MORE correct than just plain old types. typescript is a language that does this and it is very common to find types in typescript that are more "proofy" than regular types in other languages.

See here: https://www.hacklewayne.com/dependent-types-in-typescript-se...

Typescript does this. Above there's a type that's only a couple of lines long that proves a string reversal function reverses a string. I think even going that deep is overkill but you can define things like Objects that must contain a key of a specific string where the value is either a string or a number. And then you can create a function that dynamically specifies the value of the key in TS.

I think TS is a good example of a language that practically uses proof based types. The syntax is terrible enough that it prevents people from going overboard with it and the result is the most practical application of proof based typing that I seen. What typescript tells us that proof based typing need only be sprinkled throughout your code, it shouldn't take it all over.