More technical details forthcoming of course, including about formalisation... We indeed do not redo the same work over and over, but rather cache intelligently. We take special care not to interfere with debugging workflows (much in the same way that, e.g., the Tier 2 JIT does, in CPython). And as for visibility into the level of source code, what do you mean? The rewritten binary portions don't always have associated code, let alone in the language of origin.

▲

calgoo 5 hours ago | parent [-]

So the output binary is basically a black box at this point? There is no way for people to verify what your model has generated is actually what we want the code to do?That also means that every time we want to make a change to our application we are forced to re-run it from your caching system, completely locking us to you for all software output?

▲

laginimaineb 5 hours ago | parent | next [-]

I don't follow.

If you don't use Maxwell everything works as is.

Maxwell does swaps in memory during runtime, not on disk.

And we of course sign every output and do externalise the proof of equivalence.

	▲	calgoo 5 hours ago \| parent [-]
		First, thanks for the quick reply! Basically, it leaves each run of the application linked to your cloud services, so does that mean that offline and isolated runs cant use it. Second, are you just sending profiles of what is running or is data that is being processed shared? Thanks!!!

▲

fc417fc802 5 hours ago | parent | prev [-]

> So the output binary is basically a black box at this point?

To the extent that a formal proof is a black box ... ?

Which leads to an intriguing thought. If our languages and other infrastructure supported formal proofs that compiler output matched input it would obviate the motivation for reproducible builds.