[rb-general] rb formalism

David A. Wheeler dwheeler at dwheeler.com
Sat Dec 15 03:38:01 CET 2018

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:

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:

--- David A. Wheeler

More information about the rb-general mailing list