> If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD?

There is a key difference: the laws are formally verified, as in Lean or Rocq (but much faster). So it's like writing a unit test or property-based test, but when it passes, you have a mathematical proof that you will get the expected output given ANY input in the infinite space of possible inputs. In traditional TDD, you make up some test case, write some asserts, and it passes if you get the expected outputs from those inputs and only those inputs. So you have to make multiple test cases for the same thing, and you still don't have any formal guarantee of your code's correctness.

> Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?

Because it is mathematically impossible due to to Gödel’s second incompleteness theorem, which states: any consistent formal mathematical system strong enough to harbor basic arithmetic cannot prove its own consistency