Mon May 27 12:16:38 EDT 2019
Also, if the referencing computation cannot be performed at compile
time, some kind of mechanism needs to be inserted to ensure that
errors get caught. E.g. to generate code that has bounds checking so
during quickcheck these asserts can be included, then for production
code they can be left out.
I.e if there is no actual proof, there could be a statistical proof.
This way the prover could be written incrementally.