| 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 |
| 2026-06-24 02:25:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 02:27:44 +0000 | <EvanR> | *decidable f |
| 2026-06-24 02:28:12 +0000 | <EvanR> | proposition on naturals |
| 2026-06-24 02:30:47 +0000 | td_ | (~td@i53870911.versanet.de) (Ping timeout: 252 seconds) |
| 2026-06-24 02:32:05 +0000 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2026-06-24 02:32:21 +0000 | td_ | (~td@i53870930.versanet.de) |
| 2026-06-24 02:32:24 +0000 | EvanR | (~EvanR@user/evanr) EvanR |
| 2026-06-24 02:33:59 +0000 | oats | (~oats@user/oats) (Read error: Connection reset by peer) |
| 2026-06-24 02:34:14 +0000 | oats | (~oats@user/oats) oats |
| 2026-06-24 02:37:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 02:37:56 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2026-06-24 02:41:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 249 seconds) |
| 2026-06-24 02:44:28 +0000 | poscat0x04 | (~poscat@user/poscat) poscat |
| 2026-06-24 02:46:24 +0000 | poscat | (~poscat@user/poscat) (Ping timeout: 268 seconds) |
| 2026-06-24 02:49:46 +0000 | Katarushisu69 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 2026-06-24 02:52:06 +0000 | Katarushisu6 | (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2026-06-24 02:52:06 +0000 | Katarushisu69 | Katarushisu6 |
| 2026-06-24 02:52:35 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 02:52:54 +0000 | foul_owl | (~kerry@94.156.149.95) (Ping timeout: 252 seconds) |
| 2026-06-24 02:57:18 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-24 02:59:54 +0000 | <monochrom> | Oh, decidable f makes the principle much less powerful. I mean much more realistic and closer to being constructive! |
| 2026-06-24 03:01:25 +0000 | <EvanR> | yes the realization of this principle is... the purported n can't not exist, so just start looping through them all in order until you find it |
| 2026-06-24 03:02:00 +0000 | <EvanR> | as you sit there waiting for the search to terminate, you might start to feel like you're looking at the "proof" that the turing machine is infinite |
| 2026-06-24 03:02:11 +0000 | <monochrom> | Yeah. |
| 2026-06-24 03:06:58 +0000 | kimiamania | (~768865ec@user/kimiamania) (Ping timeout: 248 seconds) |
| 2026-06-24 03:07:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 03:11:38 +0000 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) smalltalkman |
| 2026-06-24 03:12:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 03:12:37 +0000 | fgarcia | (~lei@user/fgarcia) fgarcia |
| 2026-06-24 03:20:50 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2026-06-24 03:23:22 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 03:24:13 +0000 | kimiamania | (~768865ec@user/kimiamania) kimiamania |
| 2026-06-24 03:24:50 +0000 | rekahsoft | (~rekahsoft@70.51.99.119) (Remote host closed the connection) |
| 2026-06-24 03:27:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-24 03:38:44 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 03:43:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-24 03:44:09 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 268 seconds) |
| 2026-06-24 03:45:56 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-24 03:50:19 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 245 seconds) |
| 2026-06-24 03:52:08 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-24 03:54:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 03:58:48 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 04:00:40 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 261 seconds) |
| 2026-06-24 04:02:20 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-24 04:09:45 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-24 04:14:09 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 265 seconds) |
| 2026-06-24 04:14:45 +0000 | fgarcia | (~lei@user/fgarcia) (Ping timeout: 245 seconds) |
| 2026-06-24 04:20:16 +0000 | michalz | (~michalz@185.246.207.201) |
| 2026-06-24 04:25:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 04:29:38 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-24 04:40:23 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 04:44:45 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 243 seconds) |
| 2026-06-24 04:49:24 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2026-06-24 04:55:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 05:01:03 +0000 | _________ | (~nobody@user/noodly) (Quit: leaving) |
| 2026-06-24 05:02:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-24 05:03:44 +0000 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-06-24 05:05:02 +0000 | _________ | (~nobody@user/noodly) _________ |
| 2026-06-24 05:12:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 05:16:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 05:27:26 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 05:31:53 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-24 05:32:24 +0000 | <dolio> | Markov's principle says that semi-decidable propositions are ¬¬-stable. |
| 2026-06-24 05:39:33 +0000 | ft | (~ft@p508db6b1.dip0.t-ipconnect.de) (Quit: leaving) |
| 2026-06-24 05:42:47 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 05:47:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 05:58:01 +0000 | Enzo | (~Enzo@re-byods-146-50-220-52.wireless.uva.nl) |
| 2026-06-24 05:58:14 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-24 05:58:19 +0000 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-06-24 05:58:58 +0000 | Enzo | (~Enzo@re-byods-146-50-220-52.wireless.uva.nl) (Client Quit) |
| 2026-06-24 05:59:23 +0000 | Enzo | (~Enzo@re-byods-146-50-220-52.wireless.uva.nl) |
| 2026-06-24 06:01:39 +0000 | Axman6 | (~Axman6@user/axman6) Axman6 |
| 2026-06-24 06:02:21 +0000 | dolio | (~dolio@130.44.140.168) dolio |
| 2026-06-24 06:02:33 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 244 seconds) |
| 2026-06-24 06:02:57 +0000 | <gentauro> | «monochrom> Or even better, don't use it, use a plain editor» I do appreciate some warnings for when I do "corner-cutting" as in `head`. But some, in a terminal IDE, are just too distracting |
| 2026-06-24 06:03:39 +0000 | Enzo | (~Enzo@re-byods-146-50-220-52.wireless.uva.nl) () |
| 2026-06-24 06:04:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 06:04:20 +0000 | <gentauro> | btw, I can see that some of you suggest a totally checker for GHC. However, if Haskell becomes a total language (apps will always terminate) then, it's no longer Turing Complete amirite? |
| 2026-06-24 06:05:53 +0000 | <gentauro> | btw, I recently saw this SPJ podcast -> https://youtu.be/xcB_LF3cdqw and I didn't knew that GHC translated: Haskell code -> Typed Lambda Calculus as System F (I knew this) -> C-- (I did NOT know this) -> LLVM instructs :o |
| 2026-06-24 06:06:20 +0000 | <gentauro> | https://en.wikipedia.org/wiki/C-- |
| 2026-06-24 06:07:04 +0000 | <gentauro> | https://www.cs.tufts.edu/~nr/c--/ |
| 2026-06-24 06:07:36 +0000 | gentauro | do NOT click on http://www.cminusminus.org/ (somebody forgot to renew the domain xD) |
| 2026-06-24 06:08:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-24 06:12:49 +0000 | puke | (~puke@user/puke) puke |
| 2026-06-24 06:13:22 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2026-06-24 06:14:50 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-06-24 06:18:32 +0000 | <gentauro> | so Haskell lives on the shoulders of OCaml? https://github.com/nrnrnr/qc-- (nice) |
| 2026-06-24 06:18:35 +0000 | <gentauro> | hehe |
| 2026-06-24 06:19:34 +0000 | puke | (~puke@user/puke) puke |
| 2026-06-24 06:19:36 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-24 06:24:18 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 248 seconds) |
| 2026-06-24 06:28:36 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2026-06-24 06:30:11 +0000 | <dolio> | Whether it's Turing complete depends on what you mean by that. |
| 2026-06-24 06:31:21 +0000 | divya | (divya@140.238.251.170) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2026-06-24 06:32:10 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 06:34:01 +0000 | <dolio> | You can have a monad that allows you to write partial functions from T to U as `T -> M U`, say. And as long as that can embed into whatever `main` runs, your programs are not really limited. |
| 2026-06-24 06:34:46 +0000 | <dolio> | It just isn't necessarily the case that there is an equivalent function `T -> U`. |
| 2026-06-24 06:34:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 06:36:04 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) CiaoSen |
| 2026-06-24 06:39:00 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2026-06-24 06:39:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 06:41:28 +0000 | puke | (~puke@user/puke) puke |
| 2026-06-24 06:42:12 +0000 | czan | (~czan@user/mange) (Remote host closed the connection) |
| 2026-06-24 06:46:52 +0000 | <gentauro> | dolio: in the sense that total programming languages has the guarantee that ALL programs will halt. |
| 2026-06-24 06:47:20 +0000 | <dolio> | That's not what they do. |
| 2026-06-24 06:49:57 +0000 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-06-24 06:51:15 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-24 06:51:41 +0000 | olivial | (~benjaminl@user/benjaminl) (Remote host closed the connection) |
| 2026-06-24 06:52:56 +0000 | <gentauro> | dolio: hmmm. For example, Idris type-checker only works on total functions right (functions that are guaranteed to terminate)? |
| 2026-06-24 06:53:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 06:54:12 +0000 | olivial | (~benjaminl@user/benjaminl) benjaminl |
| 2026-06-24 06:54:46 +0000 | gentauro | oh, if the man himself states otherwise (Edwin Brady) -> https://cs.stackexchange.com/a/23916 then I'm mistaken |
| 2026-06-24 06:57:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 06:57:33 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-06-24 06:59:52 +0000 | dextaa | (~DV@user/dextaa) (Quit: Leaving) |
| 2026-06-24 07:00:59 +0000 | dextaa | (~DV@user/dextaa) dextaa |
| 2026-06-24 07:01:02 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2026-06-24 07:02:59 +0000 | puke | (~puke@user/puke) puke |
| 2026-06-24 07:04:50 +0000 | petrichor | (~jez@user/petrichor) (Ping timeout: 248 seconds) |
| 2026-06-24 07:06:38 +0000 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 268 seconds) |
| 2026-06-24 07:08:25 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 07:11:31 +0000 | <Leary> | monochrom: Don't bother proving /asymptotic/ complexity either. Almost every such proof hides a more precise characterisation of the relationship between arguments and costs in the finite domain we actually care about. |
| 2026-06-24 07:16:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 07:21:55 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 08:02:05 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 08:02:32 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-06-24 08:07:09 +0000 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-06-24 08:17:37 +0000 | berke93 | (~default@user/berke93) berke93 |
| 2026-06-24 08:20:44 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2026-06-24 08:24:11 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 08:27:42 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2026-06-24 08:31:49 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 08:33:45 +0000 | nschoe | (~nschoe@2a01:e0a:8e:a190:2d84:fcb7:d7c5:d3f5) (Ping timeout: 248 seconds) |
| 2026-06-24 08:36:00 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2026-06-24 08:38:42 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-06-24 08:38:51 +0000 | petrichor | (~jez@user/petrichor) petrichor |
| 2026-06-24 08:44:36 +0000 | danza | (~danza@user/danza) danza |
| 2026-06-24 08:48:38 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 08:56:21 +0000 | acidjnk_new | (~acidjnk@p200300d6e74def439d2f2469ccbb92e7.dip0.t-ipconnect.de) |
| 2026-06-24 08:56:40 +0000 | acidjnk | (~acidjnk@p200300d6e74def439d2f2469ccbb92e7.dip0.t-ipconnect.de) acidjnk |
| 2026-06-24 08:57:53 +0000 | sus03228 | (zero@user/zeromomentum) (Quit: the lounge - https://webirc.envs.net) |
| 2026-06-24 09:01:22 +0000 | sus03228 | (zero@user/zeromomentum) zeromomentum |
| 2026-06-24 09:04:23 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-06-24 09:05:13 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) (Ping timeout: 248 seconds) |
| 2026-06-24 09:08:40 +0000 | chele | (~chele@user/chele) chele |
| 2026-06-24 09:12:17 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 2026-06-24 09:20:01 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 09:21:41 +0000 | emilym | (~Thunderbi@user/emilym) emilym |
| 2026-06-24 09:26:10 +0000 | emilym | (~Thunderbi@user/emilym) (Ping timeout: 248 seconds) |
| 2026-06-24 09:50:46 +0000 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2026-06-24 09:50:46 +0000 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 2026-06-24 10:06:30 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 265 seconds) |
| 2026-06-24 10:07:25 +0000 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 276 seconds) |
| 2026-06-24 10:10:34 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2026-06-24 10:10:47 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2026-06-24 10:15:52 +0000 | danza | (~danza@user/danza) (Ping timeout: 276 seconds) |
| 2026-06-24 10:17:43 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) CiaoSen |
| 2026-06-24 10:20:20 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 10:33:31 +0000 | tremon | (~tremon@83-80-159-219.cable.dynamic.v4.ziggo.nl) tremon |
| 2026-06-24 10:37:19 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2026-06-24 10:45:44 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 10:46:59 +0000 | ski | (~ski@90-224-14-130-no600.tbcn.telia.com) (Ping timeout: 245 seconds) |
| 2026-06-24 10:48:29 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 10:48:57 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 10:50:05 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-06-24 10:50:25 +0000 | dtman34 | (~dtman34@2601:447:d17d:eaf2:8123:c1ff:6dae:d26b) dtman34 |
| 2026-06-24 10:52:15 +0000 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2026-06-24 10:52:15 +0000 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2026-06-24 10:52:15 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2026-06-24 10:52:27 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 10:53:37 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 242 seconds) |
| 2026-06-24 11:01:57 +0000 | xff0x | (~xff0x@ai070051.d.east.v6connect.net) |
| 2026-06-24 11:05:47 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 11:06:35 +0000 | pfc | (~pfc@user/pfc) pfc |
| 2026-06-24 11:13:01 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 11:16:09 +0000 | xff0x | (~xff0x@ai070051.d.east.v6connect.net) (Ping timeout: 245 seconds) |
| 2026-06-24 11:21:00 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 2026-06-24 11:27:40 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2026-06-24 11:28:39 +0000 | xff0x | (~xff0x@2405:6580:b080:900:5d3c:cbd6:36e7:66a0) |
| 2026-06-24 11:30:59 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 11:31:05 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds) |
| 2026-06-24 11:32:02 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 11:33:19 +0000 | berke93 | (~default@user/berke93) (Ping timeout: 264 seconds) |
| 2026-06-24 11:34:40 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 11:35:58 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-24 11:37:42 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 11:43:39 +0000 | collide2954 | (~collide29@user/collide2954) (Quit: The Lounge - https://thelounge.chat) |
| 2026-06-24 11:50:39 +0000 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-06-24 11:50:57 +0000 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-06-24 11:51:06 +0000 | xff0x | (~xff0x@2405:6580:b080:900:5d3c:cbd6:36e7:66a0) (Ping timeout: 252 seconds) |
| 2026-06-24 11:55:50 +0000 | collide2954 | (~collide29@user/collide2954) collide2954 |
| 2026-06-24 12:06:05 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) (Ping timeout: 252 seconds) |
| 2026-06-24 12:09:33 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 12:13:23 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 12:20:55 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 12:23:41 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 12:25:24 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) Inline |
| 2026-06-24 12:30:44 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-24 12:43:20 +0000 | xff0x | (~xff0x@2405:6580:b080:900:9570:6803:955e:7fd4) |
| 2026-06-24 12:45:17 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 12:48:00 +0000 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2026-06-24 12:49:05 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 13:02:07 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) (Quit: Client closed) |
| 2026-06-24 13:02:31 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) |
| 2026-06-24 13:07:41 +0000 | schuelermine | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-06-24 13:09:30 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 13:10:27 +0000 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) szkl |
| 2026-06-24 13:23:05 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) (Ping timeout: 240 seconds) |
| 2026-06-24 13:23:16 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) CiaoSen |
| 2026-06-24 13:26:41 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) (Quit: Client closed) |
| 2026-06-24 13:26:57 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) |
| 2026-06-24 13:32:10 +0000 | hc | (~hc@mail.hce.li) (Changing host) |
| 2026-06-24 13:32:10 +0000 | hc | (~hc@user/hc) hc |
| 2026-06-24 13:46:03 +0000 | michalz | (~michalz@185.246.207.201) (Ping timeout: 252 seconds) |
| 2026-06-24 13:49:36 +0000 | schuelermine | (~Thunderbi@user/schuelermine) (Quit: schuelermine) |
| 2026-06-24 13:52:38 +0000 | michalz | (~michalz@185.246.207.197) |
| 2026-06-24 13:57:15 +0000 | tv | (~tv@user/tv) (Read error: Connection reset by peer) |
| 2026-06-24 14:04:56 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) Inline |
| 2026-06-24 14:05:41 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) (Max SendQ exceeded) |
| 2026-06-24 14:06:31 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) Inline |
| 2026-06-24 14:08:49 +0000 | yin | (~zero@user/zero) (Remote host closed the connection) |
| 2026-06-24 14:10:35 +0000 | yin | (~zero@user/zero) zero |
| 2026-06-24 14:19:09 +0000 | yin | (~zero@user/zero) (Remote host closed the connection) |
| 2026-06-24 14:21:14 +0000 | yin | (~zero@user/zero) zero |
| 2026-06-24 14:25:36 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 14:31:00 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 14:32:03 +0000 | tv | (~tv@user/tv) tv |
| 2026-06-24 14:38:30 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 250 seconds) |
| 2026-06-24 14:43:16 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 14:43:39 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-24 14:48:04 +0000 | tusko | (~uwu@user/tusko) (Remote host closed the connection) |
| 2026-06-24 14:53:28 +0000 | tusko | (~uwu@user/tusko) tusko |
| 2026-06-24 14:58:31 +0000 | rainbyte | (~rainbyte@181.47.219.31) (Read error: Connection reset by peer) |
| 2026-06-24 14:58:32 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2026-06-24 14:58:35 +0000 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2026-06-24 14:58:51 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-24 14:58:52 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 14:59:28 +0000 | rainbyte | (~rainbyte@181.47.219.31) rainbyte |
| 2026-06-24 15:00:34 +0000 | jonnie | (~jonnie@user/jonnie) jonnie |
| 2026-06-24 15:01:36 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 15:06:49 +0000 | acidsys | (~crameleon@openSUSE/member/crameleon) (Ping timeout: 248 seconds) |
| 2026-06-24 15:09:29 +0000 | ft | (~ft@p508db6b1.dip0.t-ipconnect.de) ft |
| 2026-06-24 15:11:33 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2026-06-24 15:13:04 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 15:14:48 +0000 | Digitteknohippie | (~user@user/digit) Digit |
| 2026-06-24 15:15:09 +0000 | Digit | (~user@user/digit) (Ping timeout: 252 seconds) |
| 2026-06-24 15:17:29 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 15:18:02 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2026-06-24 15:19:47 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 15:20:43 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 15:22:02 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2026-06-24 15:23:43 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 15:27:08 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 15:29:04 +0000 | acidsys | (~crameleon@openSUSE/member/crameleon) crameleon |
| 2026-06-24 15:34:33 +0000 | Digitteknohippie | Digit |
| 2026-06-24 15:47:25 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-06-24 15:49:55 +0000 | Digit | (~user@user/digit) (Ping timeout: 252 seconds) |
| 2026-06-24 15:50:03 +0000 | Digitteknohippie | (~user@user/digit) Digit |
| 2026-06-24 16:01:24 +0000 | Digitteknohippie | Digit |
| 2026-06-24 16:04:17 +0000 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2026-06-24 16:11:00 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-06-24 16:13:55 +0000 | m2 | (~travltux@user/travltux) (Quit: WeeChat 4.7.2) |
| 2026-06-24 16:14:44 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 16:16:30 +0000 | m2 | (~travltux@user/travltux) travltux |
| 2026-06-24 16:20:07 +0000 | tremon | (~tremon@83-80-159-219.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in) |
| 2026-06-24 16:24:12 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2026-06-24 16:29:24 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2026-06-24 16:29:53 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 16:40:42 +0000 | danza | (~danza@user/danza) danza |
| 2026-06-24 16:43:28 +0000 | CiaoSen | (~Jura@2a02:3100:6377:1d00:4e50:ddff:fe9b:8922) (Ping timeout: 256 seconds) |
| 2026-06-24 16:52:41 +0000 | <EvanR> | gentauro, idris comes with escape hatch, "trust me" sort of term to let you cheat |
| 2026-06-24 16:53:24 +0000 | <EvanR> | it also has support for "productive" infinite loops |
| 2026-06-24 16:54:06 +0000 | <EvanR> | long ago the official attitude was, sometimes you need your program to run before you prove it's right |
| 2026-06-24 16:55:35 +0000 | dolio | (~dolio@130.44.140.168) (Read error: Connection reset by peer) |
| 2026-06-24 16:57:20 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 2026-06-24 16:58:48 +0000 | dolio | (~dolio@130.44.140.168) dolio |
| 2026-06-24 17:01:25 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 17:06:35 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 17:08:51 +0000 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 272 seconds) |
| 2026-06-24 17:11:09 +0000 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2026-06-24 17:22:23 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-06-24 17:26:12 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 17:27:06 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-06-24 17:29:39 +0000 | xal | (~xal@mx1.xal.systems) (Ping timeout: 246 seconds) |
| 2026-06-24 17:29:44 +0000 | xal_ | (~xal@mx1.xal.systems) xal |
| 2026-06-24 17:31:16 +0000 | <monochrom> | gentauro: Rocq, Lean, Agda --- I would coin a new name and say "Turing total complete" because every Turing machine that you can prove terminates can be expressed. (You include the proof.) |
| 2026-06-24 17:32:01 +0000 | <monochrom> | The hypothetical imagined GHC totality checker is meant to be optional. |
| 2026-06-24 17:32:36 +0000 | <monochrom> | But yes if you turned it on it would be conservative and disallow something legit. |
| 2026-06-24 17:34:02 +0000 | <jaror> | There's a great answer on the proof assistants stack overflow about turing completeness: https://proofassistants.stackexchange.com/a/4005 |
| 2026-06-24 17:34:51 +0000 | <monochrom> | Leary: I agree if it means time bounds are like "4n multiplications + (3n-4) Map.inserts". But we are not going to get "7n-3.5 seconds". |
| 2026-06-24 17:35:26 +0000 | <EvanR> | one does not simply convert "multiplications" into "seconds" anymore xD |
| 2026-06-24 17:37:50 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-06-24 17:38:24 +0000 | <monochrom> | Actually I disagree now! The hope is: (1) The time bound shows up in the type (or assertions, or spec, something). (2) If you change the code slight from 4n multiplications to 3n+10 multiplications, you don't want the type to change. This is why I settle for big-Theta. |
| 2026-06-24 17:39:57 +0000 | <monochrom> | Either that, or you still say "3n+10" in the type, but the type checker goes ahead to ignore the 3 and the 10. Someone or something is going to do the ignoring. |
| 2026-06-24 17:39:58 +0000 | <jaror> | Isn't asymptotic complexity also too vague for real world applications? Data.Seq has pretty good asymptotics, but it not so good in practice. |
| 2026-06-24 17:40:36 +0000 | <monochrom> | Yes I don't contest that. |
| 2026-06-24 17:40:41 +0000 | <jaror> | But I agree that the type shouldn't contain too much information about the function itself. |
| 2026-06-24 17:41:36 +0000 | <EvanR> | asymptotic is correct. If your program operates asymptotically. Huge amounts of N. Isn't that what big tech does? |
| 2026-06-24 17:42:19 +0000 | <jaror> | what does it mean for a program to operate asymptotically? |
| 2026-06-24 17:42:21 +0000 | <monochrom> | Under the current termination-craze culture, it is already radical enough to go from "Seq.insert terminates" to "Seq.insert is log-time amortized"! |
| 2026-06-24 17:43:09 +0000 | <EvanR> | you at an operating point where the constant factors actually don't matter anymore and the warranty on big O kicks in |
| 2026-06-24 17:43:22 +0000 | <EvanR> | instead of dominating |
| 2026-06-24 17:43:41 +0000 | <jaror> | that depends on what the constants are |
| 2026-06-24 17:43:48 +0000 | <EvanR> | so be it |
| 2026-06-24 17:43:51 +0000 | <EvanR> | wait |
| 2026-06-24 17:43:54 +0000 | <EvanR> | no it doesn't |
| 2026-06-24 17:43:58 +0000 | <EvanR> | that's the point |
| 2026-06-24 17:44:15 +0000 | <EvanR> | it's phrased in terms of "any constant factor" |
| 2026-06-24 17:44:18 +0000 | <monochrom> | The "3" in "3n" in my example will always matter. But EvanR just means the "+10" in my example. |
| 2026-06-24 17:44:19 +0000 | <jaror> | I don't think many companies are doing multiplications so large that they need to use the best known algorithms |
| 2026-06-24 17:44:51 +0000 | <EvanR> | if using worse algorithms has some benefit then yeah |
| 2026-06-24 17:44:56 +0000 | <monochrom> | oh just s/multiplication/sqlite3 update/ :) |
| 2026-06-24 17:45:08 +0000 | <jaror> | the worse algorithms are better at smaller input sizes |
| 2026-06-24 17:45:17 +0000 | <EvanR> | that's what I'm saying |
| 2026-06-24 17:45:38 +0000 | <EvanR> | how are we dominated by talk of big tech, but what's important is small input sizes xD |
| 2026-06-24 17:45:43 +0000 | <monochrom> | (sqlite3 is web scale, right? RIGHT? :) ) |
| 2026-06-24 17:45:45 +0000 | <EvanR> | should it be renamed to small tech |
| 2026-06-24 17:46:02 +0000 | <EvanR> | why are we doing so little |
| 2026-06-24 17:46:12 +0000 | <jaror> | I'm saying even "Big Tech" does not need optimal algorithms in general |
| 2026-06-24 17:46:27 +0000 | <jaror> | asymptotically optimal* |
| 2026-06-24 17:46:38 +0000 | <EvanR> | I missed the part where we are talking about absolutely optimal, beyond even what's known to science |
| 2026-06-24 17:46:44 +0000 | <EvanR> | just comparing algorithms |
| 2026-06-24 17:46:47 +0000 | <jaror> | We're talking about asymptotics |
| 2026-06-24 17:47:11 +0000 | <EvanR> | classifying and organizing what's known by compiler |
| 2026-06-24 17:47:13 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-06-24 17:47:17 +0000 | <EvanR> | so we don't have to |
| 2026-06-24 17:48:03 +0000 | <EvanR> | e.g. often you come up with an algorithm from the hip and it is exponential or some polynomial complexity |
| 2026-06-24 17:48:28 +0000 | <EvanR> | it might even be fine. But usually people want to get down to linear or nlogn at least |
| 2026-06-24 17:48:43 +0000 | <EvanR> | not necessarily optimal |
| 2026-06-24 17:48:58 +0000 | <jaror> | linear or nlogn is usually asymptotically optimal |
| 2026-06-24 17:49:07 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 246 seconds) |
| 2026-06-24 17:49:07 +0000 | <EvanR> | OKAY MAN |
| 2026-06-24 17:49:16 +0000 | <EvanR> | sheesh |
| 2026-06-24 17:49:27 +0000 | <monochrom> | Yeah we're in violent agreement. |
| 2026-06-24 17:49:49 +0000 | bggd__ | (~bgg@2a01:e0a:fd5:f510:8e31:1731:15f3:2843) (Ping timeout: 268 seconds) |
| 2026-06-24 17:51:53 +0000 | <EvanR> | propose a type system which expresses how fast algorithms are at only a handful of things in the input set |
| 2026-06-24 17:52:49 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 276 seconds) |
| 2026-06-24 17:53:55 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 17:57:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 18:00:19 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Read error: Connection reset by peer) |
| 2026-06-24 18:01:48 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 18:05:28 +0000 | <monochrom> | jaror: Thanks for the reference! I think I'm now interested in partial combinatory algebras, and maybe later realizability itself too. |
| 2026-06-24 18:07:13 +0000 | <jaror> | actually after reading it (again?) I'm not sure if that was the right link to send |
| 2026-06-24 18:07:34 +0000 | <monochrom> | No worries. It interests me in its own right. |
| 2026-06-24 18:07:49 +0000 | polykernel | (~polykerne@user/polykernel) polykernel |
| 2026-06-24 18:08:47 +0000 | <monochrom> | This always happened in my life: There is a physical book I want from the library; I went to the library, I found the book on a shelf; but wait that other book 3 inches away looks more interesting! |
| 2026-06-24 18:09:58 +0000 | <monochrom> | These accidential "oops wrong book" "oops wrong link" digressions were how I finally found what I wanted to do for grad school! |
| 2026-06-24 18:11:07 +0000 | <monochrom> | (It's how I found a formal methods book and realized (pun!) that I should do formal methods.) |
| 2026-06-24 18:12:47 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 18:13:07 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-06-24 18:13:28 +0000 | <monochrom> | oohhh Andrej Bauer as in "What is algebraic about algebraic effects and handlers"! |
| 2026-06-24 18:13:37 +0000 | <jaror> | yeah he's great |
| 2026-06-24 18:16:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 18:17:51 +0000 | bggd__ | (~bgg@2a01:e0a:fd5:f510:a39d:7d5d:f06e:ea1e) |
| 2026-06-24 18:20:20 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 18:22:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 18:27:16 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-06-24 18:35:03 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-06-24 18:37:37 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 18:39:23 +0000 | danza | (~danza@user/danza) (Read error: Connection reset by peer) |
| 2026-06-24 18:40:21 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-06-24 18:42:28 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-06-24 18:43:13 +0000 | dextaa | (~DV@user/dextaa) (Ping timeout: 272 seconds) |
| 2026-06-24 18:44:10 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 276 seconds) |
| 2026-06-24 18:48:23 +0000 | finsternis | (~X@23.226.237.192) finsternis |
| 2026-06-24 18:51:07 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 18:53:14 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 256 seconds) |
| 2026-06-24 18:58:05 +0000 | erbium | (~erbium@user/erbium) (Read error: Connection reset by peer) |
| 2026-06-24 19:00:13 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2026-06-24 19:00:29 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2026-06-24 19:01:19 +0000 | erbium | (~erbium@user/erbium) erbium |
| 2026-06-24 19:08:02 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 2026-06-24 19:08:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 19:09:01 +0000 | emilym | (~Thunderbi@user/emilym) emilym |
| 2026-06-24 19:11:59 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Ping timeout: 245 seconds) |
| 2026-06-24 19:13:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-24 19:13:25 +0000 | emilym | (~Thunderbi@user/emilym) (Ping timeout: 252 seconds) |
| 2026-06-24 19:13:26 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-06-24 19:18:56 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 19:22:29 +0000 | __monty__ | (~toonn@user/toonn) (Ping timeout: 272 seconds) |
| 2026-06-24 19:23:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 19:23:35 +0000 | EvanR | (~EvanR@user/evanr) (Remote host closed the connection) |
| 2026-06-24 19:23:54 +0000 | EvanR | (~EvanR@user/evanr) EvanR |
| 2026-06-24 19:27:36 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 19:31:06 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2026-06-24 19:33:52 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-06-24 19:38:25 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-06-24 19:38:36 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 19:41:19 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Quit: leaving) |
| 2026-06-24 19:43:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-24 19:48:51 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-24 19:49:01 +0000 | <yin> | monochrom: life is nothing without serendipity |
| 2026-06-24 19:50:21 +0000 | <EvanR> | > "life" \ "serendipity" |
| 2026-06-24 19:50:22 +0000 | <lambdabot> | <hint>:1:23: error: |
| 2026-06-24 19:50:23 +0000 | <lambdabot> | parse error (possibly incorrect indentation or mismatched brackets) |
| 2026-06-24 19:50:37 +0000 | <EvanR> | > "life" \\ "serendipity" |
| 2026-06-24 19:50:38 +0000 | <lambdabot> | "lf" |
| 2026-06-24 19:53:57 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 19:59:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-06-24 20:01:55 +0000 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2026-06-24 20:02:17 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-24 20:09:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 20:15:35 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-24 20:15:58 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-06-24 20:18:53 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 252 seconds) |
| 2026-06-24 20:19:21 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 248 seconds) |
| 2026-06-24 20:23:43 +0000 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 257 seconds) |
| 2026-06-24 20:24:09 +0000 | vgtw | (~vgtw@user/vgtw) vgtw |
| 2026-06-24 20:24:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 20:29:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-24 20:34:12 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) Enigmagic |
| 2026-06-24 20:35:20 +0000 | mikess | (~sam@user/mikess) mikess |
| 2026-06-24 20:37:46 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 20:39:37 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 20:41:50 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 245 seconds) |
| 2026-06-24 20:44:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 20:48:59 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-24 20:54:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 20:55:55 +0000 | acidjnk_new3 | (~acidjnk@p200300d6e74def9879996526b8fe093b.dip0.t-ipconnect.de) |
| 2026-06-24 20:59:04 +0000 | acidjnk | (~acidjnk@p200300d6e74def439d2f2469ccbb92e7.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-06-24 20:59:23 +0000 | acidjnk_new | (~acidjnk@p200300d6e74def439d2f2469ccbb92e7.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2026-06-24 20:59:40 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-06-24 20:59:52 +0000 | acidjnk | (~acidjnk@p200300d6e74def9879996526b8fe093b.dip0.t-ipconnect.de) acidjnk |
| 2026-06-24 21:02:17 +0000 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 244 seconds) |
| 2026-06-24 21:10:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 21:10:41 +0000 | yanmaani | (~yanmaani@gateway/tor-sasl/yanmaani) (Ping timeout: 245 seconds) |
| 2026-06-24 21:11:35 +0000 | yanmaani | (~yanmaani@gateway/tor-sasl/yanmaani) yanmaani |
| 2026-06-24 21:14:58 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-24 21:15:22 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2026-06-24 21:24:54 +0000 | cavallie | (~cavallie@user/cavallie) cavallie |
| 2026-06-24 21:25:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 21:25:29 +0000 | ricardomaps | (~ricardoma@2804:14d:a040:81ea:debe:25b7:8d22:7fa5) |
| 2026-06-24 21:29:40 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-06-24 21:38:37 +0000 | forell | (~forell@user/forell) (Quit: ZNC - https://znc.in) |
| 2026-06-24 21:39:16 +0000 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2026-06-24 21:39:34 +0000 | forell | (~forell@user/forell) forell |
| 2026-06-24 21:40:36 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 21:40:37 +0000 | cavallie | (~cavallie@user/cavallie) (Ping timeout: 245 seconds) |
| 2026-06-24 21:45:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 21:52:46 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Remote host closed the connection) |
| 2026-06-24 21:56:07 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-24 21:56:08 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 21:56:58 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Client Quit) |
| 2026-06-24 21:59:48 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) Enigmagic |
| 2026-06-24 22:00:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-24 22:01:22 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-24 22:04:12 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 256 seconds) |
| 2026-06-24 22:09:30 +0000 | spew | (~spew@user/spew) spew |
| 2026-06-24 22:11:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 22:14:32 +0000 | Digit | (~user@user/digit) Digit |
| 2026-06-24 22:15:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 22:16:08 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Quit: leaving) |
| 2026-06-24 22:18:19 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-06-24 22:20:13 +0000 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-06-24 22:21:11 +0000 | Digit | digitteknohippie |
| 2026-06-24 22:22:37 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) Enigmagic |
| 2026-06-24 22:26:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 22:26:59 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 245 seconds) |
| 2026-06-24 22:29:20 +0000 | mikess | (~sam@user/mikess) (Ping timeout: 245 seconds) |
| 2026-06-24 22:31:09 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 22:31:55 +0000 | michalz | (~michalz@185.246.207.197) (Remote host closed the connection) |
| 2026-06-24 22:42:16 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 22:45:48 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-24 22:47:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 22:47:57 +0000 | digitteknohippie | Digit |
| 2026-06-24 22:52:07 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2026-06-24 22:52:08 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2026-06-24 22:54:37 +0000 | divlamir_ | (~divlamir@user/divlamir) divlamir |
| 2026-06-24 22:54:50 +0000 | divlamir | (~divlamir@user/divlamir) (Ping timeout: 267 seconds) |
| 2026-06-24 22:57:24 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-24 22:57:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 22:59:54 +0000 | divlamir_ | (~divlamir@user/divlamir) (Ping timeout: 252 seconds) |
| 2026-06-24 23:02:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-24 23:08:39 +0000 | ricardomaps | (~ricardoma@2804:14d:a040:81ea:debe:25b7:8d22:7fa5) (Ping timeout: 244 seconds) |
| 2026-06-24 23:09:48 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) Enigmagic |
| 2026-06-24 23:13:11 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 23:14:55 +0000 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-06-24 23:15:15 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) (Read error: Connection reset by peer) |
| 2026-06-24 23:17:09 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) |
| 2026-06-24 23:17:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-24 23:18:05 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 245 seconds) |
| 2026-06-24 23:23:15 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |