[deltaonefour]

This stuff is foundational to things that check for program correctness. For examples type checkers check if the program is type correct. The foundations of these checkers rest on the content of these pages.

It goes even further then this in the sense that with logic you can design a language with correctness checking where even the logic of your entire program can be verified via something similar to a type check. So for example, Agda or Idris are examples of languages with this capability.

So basically most of this stuff isn't relative to most job. It's a higher level thing. It's more advanced theory for the people who create the tools SO you can do your job. A step above Dev Ops... it's the people who create the languages you use.