[Risord]

I think "proof" shouldn't be taken too literally. At the end stronger type system make easier to craft correctly working programs and less lottery machines.