There have been many complaints regarding Julia safety. I’ve been thinking about this and my solution proposal is with more multiple dispatch. Basically, you will generate the proof of correctness of an algorithm given a particular type via multiple dispatch. The output would be a computer-verifiable proof.
function proof_this_algorithm_work(f,Vector{T}) where {T}
theorem_statement = statement(f,Vector{T})
proof_assoc = proof_associativity(f,T)
proof_algorithm = proof(f,Vector{T};lemmas = Assoc{f,T})
return theorem_statement + proof_assoc+proof_algorithm
end
Here, in this minimal example, the users can overload either the proof associativity lemma or the proof algorithm lemma, and the proof generator will generate proof, which could then be verified, perhaps with coq, lean, or some other proof checker. If a new type is non-associative but is correct under the algorithm, however, you can overload the proof generator to use different proof pathway to prove the correctness of the algorithm. This might allow critical libraries to be made safe while retaining the permissiveness of Julia code.