3 ms·
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
by b_e_n_t_o_n 1y ago
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 1y agoWith 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 1y agoThis is way beyond my capacity for understanding ;)
- deterministic 1y agoHere is a good place to start: https://adam.math.hhu.de/#/g/leanprover-community/nng4 https://adam.math.hhu.de/#/g/leanprover-community/nng4