| 2024-05-18 00:11:08 +0200 | AlexNoo_ | (~AlexNoo@5.139.232.131) |
| 2024-05-18 00:13:08 +0200 | kadir | (~kadir@88.251.51.100) (Quit: WeeChat 4.2.2) |
| 2024-05-18 00:14:28 +0200 | AlexZenon | (~alzenon@178.34.162.221) (Ping timeout: 268 seconds) |
| 2024-05-18 00:14:49 +0200 | AlexNoo | (~AlexNoo@178.34.162.221) (Ping timeout: 256 seconds) |
| 2024-05-18 00:15:19 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) |
| 2024-05-18 00:21:11 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 256 seconds) |
| 2024-05-18 00:22:47 +0200 | AlexZenon | (~alzenon@5.139.232.131) |
| 2024-05-18 00:26:10 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-05-18 00:26:25 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds) |
| 2024-05-18 00:31:07 +0200 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds) |
| 2024-05-18 00:46:03 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) |
| 2024-05-18 00:47:23 +0200 | m257 | (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) |
| 2024-05-18 00:48:29 +0200 | <talismanick> | typeclass laws let us make intuitive assumptions about the behavior of any instance satisfying them, but you do have to prove it |
| 2024-05-18 00:48:31 +0200 | <talismanick> | but, in math, figuring out how to prove something is a big part of understanding it |
| 2024-05-18 00:49:03 +0200 | <talismanick> | just writing out the proofs for Reader, Writer, and State, I don't feel like I understand anything more for doing so |
| 2024-05-18 00:58:08 +0200 | yin | (~yin@user/zero) (Remote host closed the connection) |
| 2024-05-18 01:01:01 +0200 | <monochrom> | I would not take "prove implies understanding" religiously. When it works, it works. When it doesn't, it doesn't, or at most maybe look for another proof approach that brings understanding. |
| 2024-05-18 01:02:36 +0200 | <monochrom> | Hell, in fact, we know in math of a lot of elementary proofs that only achieve being elementary, not furthering understanding, precisely because they avoid "advanced" structures that bring understanding. |
| 2024-05-18 01:07:07 +0200 | <talismanick> | what are some instances with nontrivial proofs? |
| 2024-05-18 01:08:04 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-18 01:09:52 +0200 | ski | . o O ( "Mathematics, morally" by Eugenia Cheng in 2004-01 at <https://eugeniacheng.com/wp-content/uploads/2017/02/cheng-morality.pdf> ) |
| 2024-05-18 01:15:58 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc64113083a2457f0359.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-05-18 01:17:08 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Remote host closed the connection) |
| 2024-05-18 01:17:58 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-18 01:18:54 +0200 | <dolio> | I've been reading a book with some people, and it seems like most of the proofs are less believable than the facts they state. |
| 2024-05-18 01:21:31 +0200 | Lycurgus | (~georg@user/Lycurgus) |
| 2024-05-18 01:21:47 +0200 | <Lycurgus> | 'understanding' - that's a feel innit? |
| 2024-05-18 01:22:41 +0200 | <Lycurgus> | a feel of cognition |
| 2024-05-18 01:24:24 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer) |
| 2024-05-18 01:24:37 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-18 01:25:08 +0200 | <Lycurgus> | feel, qualia, obscure thing |
| 2024-05-18 01:26:05 +0200 | <Lycurgus> | without qualification that is; demonstrated understanding brings you back |
| 2024-05-18 01:27:00 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-05-18 01:40:05 +0200 | <Hecate> | tomsmeding: eyo, do you want a PR to enable linear-base for GHC 9.10 on the playground? |
| 2024-05-18 01:40:31 +0200 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-05-18 01:42:17 +0200 | <ski> | presumably understanding is objective insofar as it allows someone to better predict, diagnose, design |
| 2024-05-18 01:54:55 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) (Quit: WeeChat 4.2.2) |
| 2024-05-18 01:55:43 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-05-18 02:00:25 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-05-18 02:13:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-05-18 02:14:50 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-18 02:49:47 +0200 | m257 | (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds) |
| 2024-05-18 02:58:35 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 2024-05-18 03:06:34 +0200 | otto_s | (~user@p5b0448c7.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-05-18 03:08:24 +0200 | otto_s | (~user@p5b044b71.dip0.t-ipconnect.de) |
| 2024-05-18 03:14:35 +0200 | Ranhir | (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 2024-05-18 03:14:37 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 2024-05-18 03:15:40 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:cfe3:13e2:96f6:9d2c) (Quit: Leaving) |
| 2024-05-18 03:35:59 +0200 | addfb3 | (~dante@user/addfb3) (Ping timeout: 256 seconds) |
| 2024-05-18 03:40:46 +0200 | Ranhir | (~Ranhir@157.97.53.139) |