I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.

> A proof of a basic todo list or something like that.

Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?

That is always my problem too. I can see how to prove sort, if I was writing the standard library for my language I might do that (it is hard, but I hope whoever wrote my library did). However sort is already in my library. I'm writing code that does things much harder to write into a spec.

My guess is that the formal spec for a basic TODO list app is the same size as the source code of the app itself.