Yes, even in Lean you can just refuse to prove any properties.

But if you have a stronger and more expressive type system, you are more inclined to use it, instead of looking for silly workaround like in C.