4 ms·

I am not American, I am not obsessed with success in the marketplace, but I like code that actually do something, even if it is just for fun and I am the only o

by GuB-42 3y ago

I am not American, I am not obsessed with success in the marketplace, but I like code that actually do something, even if it is just for fun and I am the only one using it, with no hope of profit. I am not against formal logic, in fact, I am probably more interested by it than most of my fellow programmers, but that's not my main focus of interest. If it was my passion, I would probably have gone for a maths PhD or something like that. No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way. On a more professional note, I code so that my company can make money and pay me, my company need users who pay to make money, therefore, I code to chase users. Proven software is expensive and very few users need that much, so we don't do it. So if most programmers don't find it fun because they are more makers than scholars and it doesn't really help making money, then it is no surprise that it isn't done often.

User23 3y ago
> No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way. I agree with the spirit of your comment. I want to add that the defining characteristic of becoming proficient at a technique is that it no longer gets in the way. Touch typing is a good example: when you totally lack proficiency hunt and peck is actually faster. In fact I’ve seen people get up to around 30-50 wpm that way. Having to constantly rehome and remember where the keys are and learn the muscle memory definitely “gets in the way” at first. I think you’ll find if you take the necessary hours that once you achieve proficiency doing things like constructing a nontrivial loop without using an invariant and variant will be considerably more and not less cumbersome. That said, for exploratory programming, which a lot of professional work frankly is, I don’t find it particularly helpful to worry about proofs until I have a solid grasp on what it is I might want to prove.

by GuB-42 3y ago

User23 3y ago

> No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way. I agree with the spirit of your comment. I want to add that the defining characteristic of becoming proficient at a technique is that it no longer gets in the way. Touch typing is a good example: when you totally lack proficiency hunt and peck is actually faster. In fact I’ve seen people get up to around 30-50 wpm that way. Having to constantly rehome and remember where the keys are and learn the muscle memory definitely “gets in the way” at first. I think you’ll find if you take the necessary hours that once you achieve proficiency doing things like constructing a nontrivial loop without using an invariant and variant will be considerably more and not less cumbersome. That said, for exploratory programming, which a lot of professional work frankly is, I don’t find it particularly helpful to worry about proofs until I have a solid grasp on what it is I might want to prove.