Hmmm, this is interesting, because one might think of Software as a series of lower-level "laws", that is, specified in terms of the lines of the source code it

Hmmm, this is interesting, because one might think of Software as a series of lower-level "laws", that is, specified in terms of the lines of the source code itself in whatever programming language it was written in, and (more recently, in the AI coding era) a set of higher-level, specified in human language "laws" that a coding assistant AI must also take into consideration (in addition to the code itself) when working on the code. Because it is never 100% guaranteed that an AI produces the right answer or the right set of changes, the need for an intermediary level of "laws" between the low level and the high level arises, and that is the domain occupied by mathematical and programmatic Proof Checkers, aka "Proof Assistants" aka "Theorem Provers" (Lean, Rocq, Agda, Idris, Metamath, F*, etc., etc.) and the corresponding software harnesses that drive them... Bend is one example of what's emerging in this space. As one of the contenders in this emergent space, Bend looks like it should be worth following...