| 2026-06-24 00:02:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-24 00:13:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:14:15 +0000 | schuelermine | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-06-24 00:17:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-06-24 00:19:23 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2026-06-24 00:28:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:33:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 00:44:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:51:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-24 00:52:45 +0000 | xff0x | (~xff0x@2405:6580:b080:900:9353:b8c8:c41e:444d) (Ping timeout: 252 seconds) |
| 2026-06-24 00:57:46 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 00:58:58 +0000 | acidjnk_new | (~acidjnk@p200300d6e74def43ec2141b26299b177.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2026-06-24 00:59:28 +0000 | acidjnk | (~acidjnk@p54ad50b4.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2026-06-24 01:01:58 +0000 | prdak | (~Thunderbi@user/prdak) (Remote host closed the connection) |
| 2026-06-24 01:02:17 +0000 | prdak | (~Thunderbi@user/prdak) prdak |
| 2026-06-24 01:02:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:06:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 271 seconds) |
| 2026-06-24 01:08:21 +0000 | <monochrom> | My answer to "why you accept static and strong typing but not totality, it sounds inconsistent" is that trade-offs and cost-vs-benefit considerations are consistent. Strong static typing gives me a lot of benefits with very little cost and/or inconvenience. Totality is a lot of cost for what it's worth. |
| 2026-06-24 01:09:49 +0000 | <monochrom> | IMO totality is never going to be worthwhile because, for the same price, you should go for big-Theta complexity instead. I.e., don't bother proving termination; if anything, go straight for proving linear time or log time or whatever. Who cares about termination if it ends up being triple-expoenential time. |
| 2026-06-24 01:09:55 +0000 | ski | (~ski@90-224-14-130-no600.tbcn.telia.com) (Ping timeout: 264 seconds) |
| 2026-06-24 01:11:42 +0000 | <monochrom> | Almost every termination proof hides a time bound so it is counterproductive to throw the time bound away. |
| 2026-06-24 01:12:13 +0000 | <monochrom> | (It is not like you have a non-constructive proof of termination using the axiom of choice, is it? >:) ) |
| 2026-06-24 01:12:46 +0000 | user363627 | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2026-06-24 01:13:02 +0000 | user363627 | (~user@user/user363627) user363627 |
| 2026-06-24 01:17:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:17:55 +0000 | <jreicher> | A type system that checked complexity would be really interesting. |
| 2026-06-24 01:20:33 +0000 | ski | (~ski@90-224-14-130-no600.tbcn.telia.com) ski |
| 2026-06-24 01:21:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 01:23:49 +0000 | jonnie | (~jonnie@user/jonnie) (Remote host closed the connection) |
| 2026-06-24 01:24:23 +0000 | user363627 | (~user@user/user363627) (Remote host closed the connection) |
| 2026-06-24 01:25:45 +0000 | hiredman | (~hiredman@frontier1.downey.family) (Ping timeout: 252 seconds) |
| 2026-06-24 01:29:20 +0000 | hiredman | (~hiredman@frontier1.downey.family) hiredman |
| 2026-06-24 01:33:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:33:37 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-24 01:34:09 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2026-06-24 01:37:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 01:39:34 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-24 01:42:41 +0000 | <EvanR> | monochrom, to solve for totality first solve for complexity then set n = finite |
| 2026-06-24 01:43:15 +0000 | <EvanR> | monochrom, ~~axiom of choice~~ markov's principle |
| 2026-06-24 01:43:44 +0000 | <EvanR> | if you base the argument on that, it might actually be convincing |
| 2026-06-24 01:44:12 +0000 | <monochrom> | Err sorry, what is markov's principle again? |
| 2026-06-24 01:46:02 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 2026-06-24 01:46:38 +0000 | <EvanR> | for any function on naturals f, if there not existing an n such that f(n)=0 would be a contradiction, then there's some n where f(n) = 0 |
| 2026-06-24 01:46:55 +0000 | <jreicher> | EvanR: I don't think anybody said "solve for complexity" in the general case |
| 2026-06-24 01:47:20 +0000 | <EvanR> | that was a joke in analogy to solve the problem for all n then set n = 2 |
| 2026-06-24 01:48:16 +0000 | <monochrom> | Yeah how to visualize 6 dimensions? Visualize n dimensions, then set n=6. >:) |
| 2026-06-24 01:48:26 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:51:43 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-24 01:52:24 +0000 | <jreicher> | :) |
| 2026-06-24 01:53:09 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 257 seconds) |
| 2026-06-24 02:00:18 +0000 | Flow | (~none@gentoo/developer/flow) (Quit: WeeChat 4.7.2) |
| 2026-06-24 02:01:44 +0000 | schuelermine | (~Thunderbi@user/schuelermine) (Ping timeout: 256 seconds) |
| 2026-06-24 02:01:59 +0000 | td_ | (~td@i53870934.versanet.de) (Ping timeout: 245 seconds) |
| 2026-06-24 02:03:44 +0000 | Flow | (~none@gentoo/developer/flow) flow |
| 2026-06-24 02:03:46 +0000 | td_ | (~td@i53870911.versanet.de) |
| 2026-06-24 02:03:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 02:08:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 02:19:12 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |