Hacker News new | past | comments | ask | show | jobs | submit login

> It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running.

Interesting that you contradict yourself in successive sentences

By running the program, you, in fact, demonstrate that you are quite interested in proving whatever it is you wrote




> Interesting that you contradict yourself in successive sentences

No, I didn't. You managed to either completely miss my point, or to completely ignore it.

Just in case you didn't ignore it, let me try again. I could care about a proof for the sake of the proof. If that were the case, I probably wouldn't write a program, I'd just write the proof. (Yes, that could be mechanically turned into a program, but I didn't actually do that, because I cared about the proof rather than the program.)

When I write a program, I usually care about it as a program, not as a proof. When I write a GUI, say, I care about how it enables the users to access the rest of the program's features. You can turn that into a proof, and the compiler may in fact do so, but what it proves is something that is really unrelated to what I'm trying to do. The "proof" won't prove anything about usability or human factors or pleasing color scheme or user workflow or efficient use of screen real estate. It will prove something that, from the programming point of view, is completely uninteresting.

So, as I said, I'm not interested in the proof, I'm interested in the program. And, despite the correspondence, they are not the same thing.


>I'm not interested in the proof, I'm interested in the program

Maybe not in the abstract - but you are, in fact, "interested in the proof": because when the program doesn't do what you want it to, you either have to fix it so it does prove your use case, or you've proven that what you were trying to do was incorrect


You don’t care what the statement it proves is, and just an assurance of the conclusion would often be not valued




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: