Intent, implementation and behaviour

A codebase can have every line exercised by its tests and still have very little of what it promises stated, let alone verified, which is the gap a single coverage percentage is worst at showing. mathema separates what you know about code into three layers and measures each one on its own, so a strength in one can't hide a gap in another.

Layer	The question	Measured by
Implementation	How much of the code has anything actually exercised?	the share of statements reached by a test, a probe or a derive proof, taken together
Intent	How much of what the code is meant to do is stated?	how much of what each function is meant to do is explicitly specified and up to date
Clarity (behaviour)	Of everything knowable about a function's behaviour, how much has been pinned down?	an information score over five dimensions: what it computes, what it accepts, its bounds and shape, how safely it runs, and where it can go wrong

The layers are independent in practice as well as in principle. Tests that call every function with a couple of convenient inputs push implementation to 100 without adding anything to intent, and a function with a detailed docstring and no claims has intent on paper and nothing verified behind it. Clarity counts a falsified claim as knowledge, because knowing exactly where a function breaks is part of knowing the function, and leaves the question of whether that break is acceptable to the verdicts themselves.

Seeing all three at once

mathema-ci measure computes the three scores for a project and draws them as a triangle, with implementation and intent along the base and clarity at the apex, so a lopsided profile has a lopsided shape. The overall number is the share of the full triangle that the three scores fill, clarity * (implementation + intent) / 2 on the fractions, which collapses toward zero when any layer is empty rather than averaging politely over it. mathema's built-in writer, mathema badges, draws the same triangle but is off by default and only runs with MATHEMA_BADGES=on set. With it on, the billing module that Add claims to an existing codebase builds up, after its first sweep and with its tests counted, draws as:

        CLARITY 37
              ◆
             · ·
            ·   ·
           ·     ·
          ·       ·
         ·         ·
        ·           ·
       ·             ·
      ·               ·
     ·        ●        ·
    ·      ····         ·
   ·     ·······         ·
  ·   ···········         ·
 · ···············         ·
●·············+···●·········◆
  IMPL 100           INTENT 31
        overall 24

Every line is exercised, intent is about a third specified and clarity a little over a third pinned down, and the overall comes out at 24, 0.37 * (1.00 + 0.31) / 2, where the mean of the three would have said 56.

Intent and clarity roll up to the project by a mean weighted by how central each function is in the call graph, so a function the rest of the code leans on counts for more than a leaf helper, while implementation stays a plain ratio of lines. Clarity has a ceiling set by how much of a function's behaviour the claim vocabulary can express at all, so 100 belongs to pure, fully claimed functions and anything above 60 is doing well; a function cannot reach 100 while a function it calls has no settled definedness row in its own record, whether that callee is your own or a library's (a library's rows come from a compendium claims file, verified).

mathema badges documents how each score is computed, and mathema coverage the implementation layer on its own.