Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and

Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.