`check` return success/failure values rather than throwing error

[jariji]

I can imagine wanting to use check in a programmatic way, handling the failure dynamically rather than throwing an error. For example a failure value Err(TimeoutFailure(5s)) could be handled by the caller by trying again or trying something else. If some users want a function that throws, that can be provided too - it's easier to turn a failure value into a throw than the other way around.

Before he left, Takafumi wrote https://github.com/JuliaPreludes/Try.jl which provides a very nice way of managing these things.

[Keno]

I think the biggest issue is that there's a lot of reasons things could fail:

• We could have a counter example to the assertion
• The prop itself could have errored (which is technically the same as a counterexample, but I think it feels different to the user)
• The prover could have insufficient strength to prove or disprove the assertion

I'm not sure it's clear to me what the correct conditions are here, but I also think this is the kind of thing that very easily shakes out with use as people find what they want to use this for.

[jariji]

I'm not proposing any particular decomposition of the error types. I think no matter which types of failures people ultimately want to handle, it will be easiest to do so if it's designed so that it's possible to use check by only passing values around, not throwing any errors. Just returning Union{Ok{T}, Err{E}} where {T,E} means I don't have to catch exceptions if I want to program with failures.

This proposal is really part of a larger interest in making Julia use failure values over exceptions (discussed at length in https://github.com/JuliaLang/julia/discussions/43773) but a generic InterfaceSpecs interface seems like a particularly useful place to get in on that because of the opportunity to dispatch on interfaces.

reduce(f, xs) = @match check(associative(f, eltype(xs))) begin
    ::Ok => parallel_reduce(f, xs) 
    ::Err{CounterExample} => sequential_reduce(f, xs)
    ::Err{CheckTimeout} => sequential_reduce(f, xs)
end

but that won't work if the checks might throw.