[taybin]

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.

[bluGill]

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.

[mrkeen]

> 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?

[antonvs]

I have a proof that shows that most of what you put on your todo list, you won't do. Please let me know where I should collect my Nobel Prize.

[taybin]

To-does. Just like how a butler buttles.

[antonvs]

Excuuuuuse me, I believe that should be to-dos.

[warkdarrior]

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.

[antonvs]

I would not be even slightly surprised if it were larger.