[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!

[b_e_n_t_o_n]

This is way beyond my capacity for understanding ;)

[deterministic]

Here is a good place to start:

https://adam.math.hhu.de/#/g/leanprover-community/nng4