[rb-general] rb formalism

[David A. Wheeler]

On Fri, 14 Dec 2018 21:12:53 +0000, "Bernhard M. Wiedemann" <bernhardout at lsmod.de> wrote:
> yesterday I stumbled into a session (terminologyII?) with Eric and
> some others that did not stop at defining words. They went on to write
> up some math-like formalism using characters like
> 
> □ maybe some placeholder for data
> ■ some concrete data - e.g. gcc-4.7-4.7.2-5
> ⇨ a "build" function with variables - think f(a, b) = a+b
> ➡ a "build" function with variables filled in with concrete data
>    - think f(2, 3) = 2+3  - but not yet evaluated/computed.

It's not the same thing, but in my paper
"Fully Countering Trusting Trust through Diverse Double-Compiling" here:
https://dwheeler.com/trusting-trust/dissertation/html/wheeler-trusting-trust-ddc.html

I formally modeled compilation using first-order logic, and then used
that to prove certain properties.  That work might be of use in this case as well.

More general information about my approach is here:
https://dwheeler.com/trusting-trust/

--- David A. Wheeler