We have many of those that are perfectly fine. Writing proofs is still quite hard, especially proofs that actually say something about your program.