alt Hacker NewsI 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.
Replies
mrkeen • today at 5:25 PM
> 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?
➕ show 1 reply
warkdarrior • today at 4:21 PM
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.
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.