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.