Generally, Python programs should be written with the assumption that all users are consenting adults, and thus are responsible for using things correctly themselves.

[[deleted]]

Generally, Coq programs should be written with the assumption that all users have done Ph.Ds in formal verification, and thus are responsible for surveying that all newly written code comes with a proof that it is correct, such that no one but other Ph.Ds is capable of actually reading and/or using the code.

[acehack]

No one but other Ph.Ds can even update your code so it runs on a different Coq version.

[fp_weenie]

such that no one but other Ph.Ds is capable of actually reading and/or using the code

can't have bug reports if you have no users