| 2025-05-04 00:00:15 +0200 | tromp | (~textual@2001:1c00:3487:1b00:31c9:5f27:18bf:4d4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:04:06 +0200 | P1RATEZ | (piratez@user/p1ratez) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 2025-05-04 00:09:27 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 00:15:09 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-05-04 00:16:12 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 00:22:19 +0200 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2025-05-04 00:22:48 +0200 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2025-05-04 00:23:52 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:32:36 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-05-04 00:56:36 +0200 | nacation | (~m-3l4s76@user/nacation) (Ping timeout: 252 seconds) |
| 2025-05-04 00:57:45 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 01:00:43 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 01:00:51 +0200 | nacation | (~m-3l4s76@user/nacation) nacation |
| 2025-05-04 01:08:53 +0200 | preflex_ | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-05-04 01:10:37 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 01:12:29 +0200 | preflex | (~preflex@user/mauke/bot/preflex) (Ping timeout: 245 seconds) |
| 2025-05-04 01:12:47 +0200 | preflex_ | preflex |
| 2025-05-04 01:14:40 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 01:14:41 +0200 | ljdarj1 | ljdarj |
| 2025-05-04 01:15:34 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-05-04 01:15:43 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2025-05-04 01:33:43 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-05-04 01:40:00 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) |
| 2025-05-04 01:42:22 +0200 | hiredman | (~hiredman@frontier1.downey.family) (Quit: Lost terminal) |
| 2025-05-04 01:46:12 +0200 | la1n2 | (~la1n@176.59.166.253) (Read error: Connection reset by peer) |
| 2025-05-04 01:47:58 +0200 | la1n2 | (~la1n@176.59.56.11) |
| 2025-05-04 01:53:42 +0200 | AlexZenon_2 | (~alzenon@5.139.233.9) |
| 2025-05-04 01:55:15 +0200 | la1n23 | (~la1n@109.197.206.191) |
| 2025-05-04 01:55:16 +0200 | AlexZenon | (~alzenon@5.139.233.9) (Ping timeout: 252 seconds) |
| 2025-05-04 01:55:22 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-04 01:57:50 +0200 | la1n2 | (~la1n@176.59.56.11) (Ping timeout: 252 seconds) |
| 2025-05-04 01:58:55 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 01:59:29 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) |
| 2025-05-04 02:07:14 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 02:09:49 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-05-04 02:12:33 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-05-04 02:14:51 +0200 | sprotte24 | (~sprotte24@p200300d16f17ff001d650b9c3df58534.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-05-04 02:17:21 +0200 | Pozyomka | (~pyon@user/pyon) pyon |
| 2025-05-04 02:20:31 +0200 | sajenim | (~sajenim@user/sajenim) sajenim |
| 2025-05-04 02:51:04 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 276 seconds) |
| 2025-05-04 02:51:33 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) gabriel_sevecek |
| 2025-05-04 03:05:46 +0200 | bilegeek | (~bilegeek@2600:1008:b01a:5c24:8c91:aa31:8c9:aaf) (Quit: Leaving) |
| 2025-05-04 03:07:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-05-04 03:20:58 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-05-04 03:21:26 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.2) |
| 2025-05-04 03:28:19 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 245 seconds) |
| 2025-05-04 03:28:26 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/jackdk) (Changing host) |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/life/jackdk) jackdk |
| 2025-05-04 03:40:49 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-05-04 03:42:02 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 03:45:53 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:46:10 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2025-05-04 04:05:01 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2025-05-04 04:05:36 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2025-05-04 04:08:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7099:7f52:1441:1e43) (Ping timeout: 248 seconds) |
| 2025-05-04 04:12:52 +0200 | typedfern_ | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-04 04:13:42 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 2025-05-04 04:15:49 +0200 | td_ | (~td@i53870919.versanet.de) (Ping timeout: 248 seconds) |
| 2025-05-04 04:17:38 +0200 | td_ | (~td@i53870915.versanet.de) |
| 2025-05-04 04:21:12 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2025-05-04 04:23:24 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 04:44:00 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 04:48:43 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 05:00:31 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-04 05:00:31 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-05-04 05:00:50 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-04 05:01:14 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-05-04 05:21:56 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-05-04 05:22:31 +0200 | xff0x | (~xff0x@2405:6580:b080:900:e1a9:cd8e:4cbb:591b) |
| 2025-05-04 05:36:10 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 2025-05-04 05:36:52 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-05-04 05:38:12 +0200 | tomku | (~tomku@user/tomku) (Ping timeout: 276 seconds) |
| 2025-05-04 05:42:36 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 05:43:34 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 05:44:33 +0200 | tomku | (~tomku@user/tomku) tomku |
| 2025-05-04 05:47:49 +0200 | aforemny_ | (~aforemny@i59F4C6FD.versanet.de) aforemny |
| 2025-05-04 05:48:06 +0200 | aforemny | (~aforemny@i59F4C605.versanet.de) (Ping timeout: 252 seconds) |
| 2025-05-04 06:08:54 +0200 | <haskellbridge> | <hellwolf> Huh? |
| 2025-05-04 06:09:05 +0200 | <haskellbridge> | <hellwolf> sonic boom? |
| 2025-05-04 06:15:26 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 06:15:58 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | <hellwolf> anyways, today is the day to confront the demon... |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/xIZbjVwEiWebhDhhUHdAQgaI/rbHeUYfmCGw (4 lines) |
| 2025-05-04 06:18:03 +0200 | <monochrom> | I think for sum types you go for prisms rather than lenses. |
| 2025-05-04 06:23:10 +0200 | <haskellbridge> | <hellwolf> makePrisms |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | <hellwolf> let me see that i can learn there. |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | also, should i use generics-sop, though i would need code examples... |
| 2025-05-04 06:27:05 +0200 | <haskellbridge> | <hellwolf> https://hackage-content.haskell.org/package/lens-5.3.4/docs/src/Control.Lens.Internal.PrismTH.html… |
| 2025-05-04 06:27:07 +0200 | <haskellbridge> | not too many lines to learn. it seems. i am relieved |
| 2025-05-04 06:29:37 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) (Ping timeout: 248 seconds) |
| 2025-05-04 06:52:13 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds) |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | <hellwolf> "isn't :: Prism s t a b -> s -> Bool" |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | finally i see others using the single quote in names... |
| 2025-05-04 06:56:45 +0200 | <monochrom> | :) |
| 2025-05-04 06:59:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-04 07:16:05 +0200 | <EvanR> | ahem |
| 2025-05-04 07:16:18 +0200 | <EvanR> | please. apostrophe |
| 2025-05-04 07:35:04 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 07:35:10 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 07:44:10 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) bitmapper |
| 2025-05-04 07:59:18 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-05-04 08:05:52 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-05-04 08:13:07 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-04 08:23:21 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 08:24:13 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-05-04 08:25:57 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) acidjnk |
| 2025-05-04 08:26:36 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 08:32:17 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 08:32:44 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 08:37:54 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-05-04 08:46:57 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 08:53:50 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 09:00:00 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-04 09:00:38 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-04 09:01:32 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 09:04:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 09:07:14 +0200 | la1n2 | (~la1n@81.222.176.125) |
| 2025-05-04 09:09:53 +0200 | la1n23 | (~la1n@109.197.206.191) (Ping timeout: 265 seconds) |
| 2025-05-04 09:22:39 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-05-04 09:23:45 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-05-04 09:24:02 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-05-04 09:25:41 +0200 | <haskellbridge> | <hellwolf> what's the reason for classy lenses or prisma? It's non obvious to me, and the docs doesn't explain the "why" |
| 2025-05-04 09:40:04 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 09:52:20 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-05-04 10:32:55 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-05-04 10:35:02 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 10:35:04 +0200 | <jackdk> | hellwolf: https://youtu.be/GZPup5Iuaqw?t=1499 (note the timecode, though the whole talk is good) |
| 2025-05-04 10:50:59 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-05-04 10:57:16 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-05-04 10:57:39 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 11:08:06 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-05-04 11:10:29 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-05-04 11:13:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) |
| 2025-05-04 11:16:27 +0200 | <haskellbridge> | <hellwolf> thank you! checking now |
| 2025-05-04 11:21:57 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-05-04 11:22:22 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-05-04 11:37:12 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-04 11:47:19 +0200 | Square | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-05-04 11:51:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 12:00:10 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:04:37 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 12:05:04 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 2025-05-04 12:14:42 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-05-04 12:15:17 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 2025-05-04 12:16:50 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:27:57 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-05-04 12:31:27 +0200 | <hellwolf> | I watched it. TL;DV: to index optical operations into one type class, so that you can stack them up in your application monad. It's probably obvious if you actually build such a application that deal with real world :) |
| 2025-05-04 12:33:27 +0200 | <Rembane> | That sounds neat |
| 2025-05-04 12:36:50 +0200 | <hellwolf> | I wish the docs actually care to give just a few lines of "why". But I guess it risks of being too brief and confuses some people. Not sure what's the good middle ground of these sort of things is. |
| 2025-05-04 12:38:34 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-05-04 12:45:48 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 12:52:13 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 265 seconds) |
| 2025-05-04 12:53:03 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 13:00:43 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 13:07:29 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-05-04 13:07:59 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 13:08:16 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 13:13:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-05-04 13:16:15 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2025-05-04 13:25:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 2025-05-04 13:38:10 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 13:45:09 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 13:51:28 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 13:51:45 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 13:52:15 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 13:58:36 +0200 | <[exa]> | are there some good "small" libraries theorem proving? E.g. I've got an algebra, a few axioms on it, and I want to see how the axioms can be combined to derive some expression in the algebra. Ideally if axiom schemes are supported. |
| 2025-05-04 13:58:47 +0200 | <[exa]> | s/if // |
| 2025-05-04 14:01:26 +0200 | <[exa]> | the issue with the theorem provers I see is that they kinda assume some particular fixed algebra (some kind of logic), I need some freedom in there without having to encode stuff too much. |
| 2025-05-04 14:04:14 +0200 | <tomsmeding> | prolog? |
| 2025-05-04 14:05:46 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 14:11:57 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 14:14:12 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-04 14:15:19 +0200 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 2025-05-04 14:16:02 +0200 | <[exa]> | s/List/Logic/ |
| 2025-05-04 14:21:16 +0200 | <tomsmeding> | I mean you can actually model a proof checker, but at that point you're writing what you're asking already exists, I guess :p |
| 2025-05-04 14:21:47 +0200 | <tomsmeding> | what kind of things do you want to prove? |
| 2025-05-04 14:22:24 +0200 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |
| 2025-05-04 14:26:50 +0200 | <haskellbridge> | <hellwolf> I wonder how well LLM nowadays to cope with these sort of things when it comes to heuristics |
| 2025-05-04 14:31:23 +0200 | <[exa]> | hellwolf: if the heuristic is "there was more chat about it on the internet", it's going great. |
| 2025-05-04 14:32:31 +0200 | <[exa]> | tomsmeding: I've just started reading up on the whole topic. Looks like I wanted more of a program synthesis. :D |
| 2025-05-04 14:35:19 +0200 | <haskellbridge> | <hellwolf> I think the hvm person is doing this entire neogen thing, banking on LLM model. |
| 2025-05-04 14:35:31 +0200 | <[exa]> | and yeah well it's actually prolog. I want to write constraints on what holds "before" and should hold "after" the program, and the thing would ideally fill in some "middle" so that the "after" is satisfied. |
| 2025-05-04 14:36:52 +0200 | <[exa]> | hellwolf: what's hvm and neogen? (googling leads to either twiddler or spam, which is sus) |
| 2025-05-04 14:37:20 +0200 | <tomsmeding> | [exa]: oh that definitely sounds like program synthesis :p |
| 2025-05-04 14:38:18 +0200 | <tomsmeding> | and I mean, coding up a simple engine that tries to deduce a sequent from given ones with BFS isn't too hrad |
| 2025-05-04 14:38:41 +0200 | <haskellbridge> | <hellwolf> https://x.com/VictorTaelin he is the frontman doing it. There is this VC vibe thing: so, there is sometimes selling before confirmation bias, but there are some interesting bits from time to time. I don't fully follow, tbh |
| 2025-05-04 14:38:52 +0200 | <[exa]> | tomsmeding: the issue is that my "instructions" won't very "simple" (usually multiple effects tied together), so just going the syntax way ("forth is instructions!") is going to be brutally bad |
| 2025-05-04 14:39:01 +0200 | <tomsmeding> | and that sounds limited, but if you want something more than can be expressed to an engine like that, things become very hard, very undecidable, very quickly |
| 2025-05-04 14:39:17 +0200 | <tomsmeding> | I see |
| 2025-05-04 14:39:28 +0200 | <haskellbridge> | <hellwolf> - bias of selling before confirmed result. |
| 2025-05-04 14:39:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 14:39:53 +0200 | <[exa]> | hellwolf: I'd classify as scam tbh |
| 2025-05-04 14:40:05 +0200 | tomsmeding | is afk for a while, sory |
| 2025-05-04 14:40:10 +0200 | <tomsmeding> | *sorry |
| 2025-05-04 14:40:28 +0200 | <haskellbridge> | <hellwolf> I know what you mean. But I will not be so quick to judge. |
| 2025-05-04 14:40:46 +0200 | <[exa]> | tomsmeding: np enjoy the sunday :D |
| 2025-05-04 14:41:12 +0200 | haskellbridge | hellwolf go doing something relax too. enjoy your sunday folks |
| 2025-05-04 14:42:42 +0200 | tremon | (~tremon@83.80.159.219) tremon |
| 2025-05-04 14:43:55 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-05-04 14:44:57 +0200 | <[exa]> | hellwolf: oh hvm is the thing with the "MAGIC" wannabe meme in the main readme |
| 2025-05-04 14:45:26 +0200 | <[exa]> | turns out I already classified it as such like 2 years ago :D |
| 2025-05-04 14:51:52 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 14:53:02 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 14:53:09 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 14:55:30 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 14:55:48 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 14:56:11 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-04 14:57:27 +0200 | <[exa]> | well screw it, I guess I'll do an A* and blame the heuristics. :D |
| 2025-05-04 14:58:51 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-05-04 14:59:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 15:02:29 +0200 | <haskellbridge> | <hellwolf> data AThing a = DoSomethingWith a Person | ScamWith a Person |
| 2025-05-04 15:06:47 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-05-04 15:11:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 15:12:09 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 15:14:59 +0200 | AlexZenon_2 | AlexZenon |
| 2025-05-04 15:19:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-05-04 15:22:42 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-05-04 15:24:07 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye) |
| 2025-05-04 15:26:26 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-05-04 15:28:54 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 15:29:11 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 15:29:59 +0200 | la1n2 | (~la1n@81.222.176.125) (Read error: Connection reset by peer) |
| 2025-05-04 15:30:02 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) TimWolla |
| 2025-05-04 15:31:49 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-05-04 15:35:56 +0200 | la1n | (~la1n@85.249.17.224) |
| 2025-05-04 15:40:27 +0200 | la1n2 | (~la1n@176.59.41.59) |
| 2025-05-04 15:40:46 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 268 seconds) |
| 2025-05-04 15:42:49 +0200 | la1n | (~la1n@85.249.17.224) (Ping timeout: 244 seconds) |
| 2025-05-04 15:51:13 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-05-04 16:22:48 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Ping timeout: 252 seconds) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-05-04 16:23:04 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 16:23:10 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 16:25:09 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 16:25:22 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 16:32:21 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 16:38:56 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 16:50:18 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 16:52:27 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 16:53:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-05-04 16:54:06 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 16:56:17 +0200 | typedfern_ | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 248 seconds) |
| 2025-05-04 16:56:42 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-04 16:56:56 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) typedfern |
| 2025-05-04 17:04:03 +0200 | noctuks | (MR7CNKXm0J@user/noctux) (Quit: WeeChat 4.5.1) |
| 2025-05-04 17:04:04 +0200 | yushyin | (qjh7DQNxXf@mail.karif.server-speed.net) (Quit: WeeChat 4.5.1) |
| 2025-05-04 17:04:04 +0200 | s4msung | (HpS7xJgsJj@user/s4msung) (Quit: s4msung) |
| 2025-05-04 17:04:24 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 17:04:40 +0200 | noctuks | (d32f0pjuYL@user/noctux) noctux |
| 2025-05-04 17:04:44 +0200 | s4msung | (K4xiEoBBTh@user/s4msung) s4msung |
| 2025-05-04 17:04:44 +0200 | yushyin | (zv27G51Tbg@mail.karif.server-speed.net) yushyin |
| 2025-05-04 17:04:54 +0200 | <Pozyomka> | Is there any good reason why Data.Sequence doesn't export a function “adjustF :: Functor f => (a -> f a) -> Int -> Seq a -> f (Seq a)”? |
| 2025-05-04 17:06:30 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 268 seconds) |
| 2025-05-04 17:08:52 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-04 17:11:34 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 17:12:42 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-04 17:16:27 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 17:28:00 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-05-04 17:30:01 +0200 | <[exa]> | Pozyomka: not really but maybe it would be redundant with other functions there? |
| 2025-05-04 17:39:08 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-05-04 17:43:50 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 17:44:03 +0200 | <[exa]> | ok well probably not the case, the internal "single-lookup adjust" in the package doesn't seem to support passing the functors through |
| 2025-05-04 17:44:23 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |