Rice's Theorem

Today, I learned about Rice's Theorem.

It essentially states that all non-trivial semantic properties of a program cannot be mechanized.

A concrete example: Say that your job is to optimize compilers. Will you ever be out of a job (ie. will you ever run out of things that you can optimize)?

To grossly handwave, you can think of optimization, as parsing the semantics of a program and finding a reduced representation. Say for instance, you have a program which runs forever. The most optimized version of the program is just an empty while loop. If you could construct an optimization which reduced all infinitely running programs down to this construct, you would have solved the Halting problem, which is impossible.

This matters since it states that you can't generate an orthogonal set of developer tools which allow you to mechanistically determine that your program is correct. You will always miss something; hence, adding more dev tools gives you a series of diminishing returns towards perfection that you will never reach.