|
@pigworker | |||||
|
From a Curry-Howard perspective, "I like programming but I don't like maths." means "I like programming but I don't like programming.".
|
||||||
|
||||||
|
⊢ 🐝, ¬🐝
@ZoltanAK
|
28. ruj 2017. |
|
But "liking" does not respect extensional equality. If I like a theorem proved using unary-ℕ, I may still dislike the proof using ternary-ℕ.
|
||
|
|
||
|
Conor Mc Bride
@pigworker
|
28. ruj 2017. |
|
Stop sentence after word 5.
|
||
|
|
||
|
Diogo (f a) Castro
@dfacastro
|
28. ruj 2017. |
|
Unless untyped languages are your thing 😱
|
||
|
|
||
|
Conor Mc Bride
@pigworker
|
28. ruj 2017. |
|
Formally, perhaps. But I'd argue that C-H has an informal aspect identifying programming and proof as similar human activities.
|
||
|
|
||
|
Jonathan Edwards
@jonathoda
|
28. ruj 2017. |
|
There are more kinds of programming in the world than are dreamt of in your philosophy
|
||
|
|
||
|
Conor Mc Bride
@pigworker
|
28. ruj 2017. |
|
There are more kinds of philosophy in the world than are dreamt of in anyone's philosophy.
|
||
|
|
||
|
Oleg Lobachev
@theoal
|
28. ruj 2017. |
|
Isn't it "I like math, but I hate math"?
|
||
|
|
||
|
Conor Mc Bride
@pigworker
|
28. ruj 2017. |
|
What's the difference?
|
||
|
|
||
|
Loch Nessa Monster🌸
@pasiphae_goals
|
28. ruj 2017. |
|
In practice this usually means "I like programming badly", of course.
|
||
|
|
||
|
Kris Nuttycombe
@nuttycom
|
28. ruj 2017. |
|
"I like ignoring potential errors."
|
||
|
|
||