Comment by zaik

I hope something comes along that has a much more powerful type system like Rocq. I also dream of tagging certificates to values such as "this string has passed SQL validation".