[Ur] need help with unification and field name disjointness proof failures

[Adam Chlipala]

On 04/06/2017 06:22 PM, Benjamin Barenblat wrote:
> The fact that `rand` returns -1 on failure, however, is a bit scary.
> That sounds like a CVE waiting to happen – people aren’t going to
> check the result code from `rand`. Adam, how would you feel about it
> returning an `option` or throwing an application error if it fails?

Raising an error seems like a reasonable idea.  It could signal to 
snooping parties that we ran out of entropy, but I hope that isn't such 
a serious leak.  Any other strong opinions from people watching the list?

BTW, Ur/Web is also already using cryptographic hashing internally, for 
CSRF cookie signatures, so perhaps it also makes sense to expose 
functionality of your other library by default.