3 ms·

Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as int

Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as intended," and then thought, "Maybe this is a problem?" Fast and loose reasoning is not morally correct; it's ethically bankrupt. Programmers in other languages don't get to forget about their errors, imperfections, and footguns; I'm not sure why Hask and Haskell should be let off the hook in our minds. (Also, since somebody's gonna accuse me of not having read "Fast and Loose Reasoning", I absolutely have, and the biggest disappointment is failing to define useful equality on function values as if they were plain values. Might be impossible in Hask, but it's trivial in Pos, the category of posets; maybe Hask isn't a very good category!)

lmm 8y ago
> Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as intended," and then thought, "Maybe this is a problem?" In some cases yes. Like I said in my original post, use Idris and then you don't have this particular instance of the problem. In general though the possibility of failure seems unavoidable; even two runs of a byte-for-byte identical program might "produce different results" if someone dynamites the computer one of them is running on. > Fast and loose reasoning is not morally correct; it's ethically bankrupt. Programmers in other languages don't get to forget about their errors, imperfections, and footguns; I'm not sure why Hask and Haskell should be let off the hook in our minds. I don't think there's anything special about Haskell here. Programmers in plenty of languages reason as though exceptions/panics will never happen, and are sometimes surprised by their program's behaviour when they do.

lmm 8y ago

> Yeah, but have you ever thought, "Y'know, maybe the fact that we can't reason in Hask but instead have to work in franken-Hask where not everything works as intended," and then thought, "Maybe this is a problem?" In some cases yes. Like I said in my original post, use Idris and then you don't have this particular instance of the problem. In general though the possibility of failure seems unavoidable; even two runs of a byte-for-byte identical program might "produce different results" if someone dynamites the computer one of them is running on. > Fast and loose reasoning is not morally correct; it's ethically bankrupt. Programmers in other languages don't get to forget about their errors, imperfections, and footguns; I'm not sure why Hask and Haskell should be let off the hook in our minds. I don't think there's anything special about Haskell here. Programmers in plenty of languages reason as though exceptions/panics will never happen, and are sometimes surprised by their program's behaviour when they do.