That's a bit like saying that pthreads is deadlock free because the Unix kernel can still schedule other programs. It is an useful guarantee, but it doesn't help fix my broken program.

Yes. If you want to encode soundness guarantees, you might want to look for a language with formal verification facilities instead, like Ada-SPARK.

I'm not sure if there are any languages that allow you to pass down / inherit language constraints specifically, maybe Lisp or similar can do that? But then often that unfortunately wouldn't be actually helpful, as these requirements usually come from the outside (like in your Python example, it comes from Python being specified such that you can encode deadlocking logic in your Python code).

For most everyone who aren't trying to implement the possibility of deadlocks in guestcode, this remains a useful property even without that.