I wasn't just talking about Idris. There isn't a single tool out there that can automatically prove that your quicksort implementation actually sorts without pretty significant work.