[rb-general] rb formalism

[Bernhard M. Wiedemann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi,

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.

and with these, it was possible to write things like
■ + ■ = ■ (composition/aggregation of data)
■ + ⇨ = ➡

and define a reproducible build as an unambiguous mapping of hashes "h"
h(➡) → h(➡■)

We also thought, that typo-fixes in libfoo-doc and diverse compilation
would then be modeled by different h(➡) mapping to the same build
output h(➡■)
But when I thought more about it, that cannot be, since ➡ is part of
the right hand hash, it would always be unique per input.
So it could rather be
h(➡) → h(■)

meaning, a reproducible build is when you take all input data and the
build function and evaluating it, always yields the same output data.

We also found that the model did not really cover unreproducible
builds (with side-inputs like time and parallelism-race-results [1])
and just declared them as bugs that needed to be fixed to be covered
by the model.

Pretty abstract and high-level, but maybe useful?

Have phun
Bernhard M.

[1]
https://github.com/bmwiedemann/theunreproduciblepackage/blob/master/race/race.sh
-----BEGIN PGP SIGNATURE-----

iF0EARECAB0WIQRk4KvQEtfG32NHprVJNgs7HfuhZAUCXBQczQAKCRBJNgs7Hfuh
ZPmsAJ0WYLDnxkz1HMg2XPyEj94HXbwttQCg9l2BvD4LFwiETW2WaxaBw6LLHnc=
=jsao
-----END PGP SIGNATURE-----