[habitue]

> by encoding more and more responsibility in the type system, you're just pushing your business logic to a different language

Yes, this is 100% correct. Type systems are just another language

> The same propensity for human error exists there as well.

This is where I disagree. Sure you can make errors in types, but it's not the same because strong type systems are more like proof systems. They tell you when you've encoded something that doesnt make logical sense. And they help you figure out if your code can be made to adhere to them. It's a checker that you don't normally have.

> But I don't see much difference in putting that logic in the base language or the higher order type system language, except the base language is more expressive and flexible.

The type language encodes your assumptions, and the base language has to adhere to those assumptions. If your type language is expressive enough, you can encode pretty complex assumptions. There's value in having the two playing against each other.

Similar to tests: you could say tests are just re-stating what you've already written in your code. In reality, it's another check for consistency with your original intention.

[b_e_n_t_o_n]

What I'm curious about is how a type system can be used to encode business logic in a way that it can tell when something is encoded in a way that doesn't make logical sense? How can a type system detect an error in my business logic if the language I'm encoding it in is the type system itself? Wouldn't I need a higher-higher order language on top of it to validate the higher-order language?

[deterministic]

With a powerful type system (think Coq/Lean/...) you can declare the following (for example):

forall s:Source, execute_machine_code(compile(s)) = interpret_source_code(s)

And the compiler will only accept your compiler code as being typed correctly if for all possible source code, running the compiled code gives the same result as interpreting the source code directly.

In other words, you are proving your compiler to be correct. Think about it as having an infinite number of test cases in a single line.

Now that's powerful!