2025/08/27

2025-08-27 00:00:39 +0200gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2025-08-27 00:01:22 +0200gmg(~user@user/gehmehgeh) gehmehgeh
2025-08-27 00:03:20 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-08-27 00:03:33 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au)
2025-08-27 00:06:54 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 258 seconds)
2025-08-27 00:08:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 00:09:24 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-08-27 00:12:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 00:15:37 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-08-27 00:20:53 +0200tromp(~textual@2001:1c00:3487:1b00:e4be:35da:9f42:3b49) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-08-27 00:21:21 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2025-08-27 00:21:28 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-08-27 00:21:56 +0200pavonia(~user@user/siracusa) siracusa
2025-08-27 00:22:55 +0200takuan(~takuan@d8D86B9E9.access.telenet.be) (Remote host closed the connection)
2025-08-27 00:23:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 00:24:33 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf) (Server closed connection)
2025-08-27 00:24:50 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf) ezzieyguywuf
2025-08-27 00:27:59 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 00:28:31 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-08-27 00:35:09 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-08-27 00:35:16 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 258 seconds)
2025-08-27 00:35:23 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au)
2025-08-27 00:38:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 00:43:36 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-08-27 00:48:18 +0200Frostillicus(~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Remote host closed the connection)
2025-08-27 00:48:41 +0200Frostillicus(~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
2025-08-27 00:54:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 00:55:27 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-08-27 00:56:41 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2025-08-27 00:57:25 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-08-27 00:59:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 01:01:04 +0200Square2(~Square@user/square) (Ping timeout: 256 seconds)
2025-08-27 01:02:47 +0200nitrix_(~nitrix@user/meow/nitrix) nitrix
2025-08-27 01:03:29 +0200nitrix(~nitrix@user/meow/nitrix) (Ping timeout: 272 seconds)
2025-08-27 01:04:24 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 258 seconds)
2025-08-27 01:04:56 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-08-27 01:07:02 +0200noctuks(aVjnm6iDRi@user/noctux) (Server closed connection)
2025-08-27 01:07:21 +0200noctuks(eCIc2Rhff8@user/noctux) noctux
2025-08-27 01:09:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 01:10:15 +0200yushyin(rAA5wfgz8R@mail.karif.server-speed.net) (Server closed connection)
2025-08-27 01:10:39 +0200yushyin(8jcHYEVNqp@mail.karif.server-speed.net) yushyin
2025-08-27 01:12:47 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-08-27 01:13:28 +0200s4msung(gjllrwEMMC@user/s4msung) (Server closed connection)
2025-08-27 01:13:47 +0200s4msung(Ci2aDJRib8@user/s4msung) s4msung
2025-08-27 01:14:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 01:14:27 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-08-27 01:15:04 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2025-08-27 01:24:14 +0200weary-traveler(~user@user/user363627) user363627
2025-08-27 01:25:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 01:29:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 01:31:40 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds)
2025-08-27 01:37:00 +0200Frostillicus(~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Remote host closed the connection)
2025-08-27 01:37:22 +0200Frostillicus(~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net)
2025-08-27 01:39:23 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-08-27 01:40:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 01:41:18 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-08-27 01:41:32 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au)
2025-08-27 01:42:04 +0200sprotte24(~sprotte24@p200300d16f0e5a00c5b8a13e20fc3383.dip0.t-ipconnect.de) (Quit: Leaving)
2025-08-27 01:44:04 +0200mange(~mange@user/mange) mange
2025-08-27 01:44:06 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-08-27 01:44:16 +0200ttybitnik(~ttybitnik@user/wolper) (Quit: Fading out...)
2025-08-27 01:44:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-08-27 01:47:04 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 248 seconds)
2025-08-27 01:48:40 +0200kaol(~kaol@94-237-45-144.nl-ams1.upcloud.host) (Ping timeout: 245 seconds)
2025-08-27 01:49:41 +0200kaol(~kaol@94-237-45-144.nl-ams1.upcloud.host)
2025-08-27 01:56:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 01:56:56 +0200xff0x(~xff0x@2405:6580:b080:900:bd9c:270d:261:4d07) (Ping timeout: 244 seconds)
2025-08-27 01:58:57 +0200trickard_trickard
2025-08-27 02:00:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-08-27 02:09:20 +0200acidjnk(~acidjnk@p200300d6e7171900c8d1e26a04eb2053.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
2025-08-27 02:10:07 +0200synner(~david@64-251-141-60.fidnet.com)
2025-08-27 02:10:29 +0200synner(~david@64-251-141-60.fidnet.com) (Leaving)
2025-08-27 02:10:32 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-08-27 02:11:25 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 02:16:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 02:23:08 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net)
2025-08-27 02:26:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 02:31:10 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-08-27 02:40:36 +0200tremon(~tremon@83.80.159.219) (Remote host closed the connection)
2025-08-27 02:41:03 +0200xff0x(~xff0x@2405:6580:b080:900:83a1:9d1e:34ac:9163)
2025-08-27 02:42:06 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-08-27 02:42:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 02:46:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-08-27 02:53:40 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-08-27 02:54:55 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-08-27 02:57:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 02:58:57 +0200xff0x(~xff0x@2405:6580:b080:900:83a1:9d1e:34ac:9163) (Quit: xff0x)
2025-08-27 02:59:28 +0200Googulator(~Googulato@2a01:36d:106:28ad:d14e:68ce:c41e:4464)
2025-08-27 03:02:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 03:02:36 +0200xff0x(~xff0x@2405:6580:b080:900:a6f3:8715:1520:fbd)
2025-08-27 03:05:32 +0200fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2025-08-27 03:07:52 +0200xff0x(~xff0x@2405:6580:b080:900:a6f3:8715:1520:fbd) (Ping timeout: 255 seconds)
2025-08-27 03:08:08 +0200segfaultfizzbuzz(~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 248 seconds)
2025-08-27 03:09:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 03:12:51 +0200fgarcia(~lei@user/fgarcia) fgarcia
2025-08-27 03:13:57 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-08-27 03:14:34 +0200trickard(~trickard@cpe-63-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-08-27 03:14:47 +0200trickard_(~trickard@cpe-63-98-47-163.wireline.com.au)
2025-08-27 03:18:28 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds)
2025-08-27 03:22:44 +0200itaipu(~itaipu@168.121.97.28) (Ping timeout: 256 seconds)
2025-08-27 03:24:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 03:26:48 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 248 seconds)
2025-08-27 03:28:48 +0200fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2025-08-27 03:28:53 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-08-27 03:28:57 +0200cyphase(~cyphase@user/cyphase) (Ping timeout: 256 seconds)
2025-08-27 03:29:30 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-08-27 03:34:18 +0200fgarcia(~lei@user/fgarcia) fgarcia
2025-08-27 03:35:24 +0200itaipu(~itaipu@168.121.97.28) itaipu
2025-08-27 03:36:15 +0200fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2025-08-27 03:36:39 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-08-27 03:40:14 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-08-27 03:40:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 03:40:18 +0200vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 256 seconds)
2025-08-27 03:41:44 +0200cyphase(~cyphase@user/cyphase) cyphase
2025-08-27 03:41:49 +0200vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-08-27 03:42:52 +0200fgarcia(~lei@user/fgarcia) fgarcia
2025-08-27 03:43:03 +0200hakutaku(~textual@chen.yukari.eu.org) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2025-08-27 03:43:44 +0200hakutaku(~textual@chen.yukari.eu.org)
2025-08-27 03:43:44 +0200fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2025-08-27 03:44:38 +0200fgarcia(~lei@user/fgarcia) fgarcia
2025-08-27 03:46:18 +0200trickard_trickard
2025-08-27 03:47:02 +0200fgarcia(~lei@user/fgarcia) (Read error: Connection reset by peer)
2025-08-27 03:47:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 03:53:59 +0200fgarcia(~lei@user/fgarcia) fgarcia
2025-08-27 03:54:53 +0200 <Axman6> I asked yesterday about whether there was a cbrt function, which exists in C++ at least, and apparently x**(1/3) is the best we can do. I thought I would take a look at what LLVM does, thinking "how hard could it be". Never mind: https://github.com/llvm/llvm-project/blob/main/libc/src/__support/math/cbrt.h
2025-08-27 03:58:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 04:01:12 +0200ec(~ec@gateway/tor-sasl/ec) (Ping timeout: 272 seconds)
2025-08-27 04:02:29 +0200ec(~ec@gateway/tor-sasl/ec) ec
2025-08-27 04:03:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-08-27 04:04:02 +0200haskellman(~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422)
2025-08-27 04:04:08 +0200pabs3(~pabs3@user/pabs3) (Ping timeout: 248 seconds)
2025-08-27 04:04:23 +0200 <haskellman> Hello, how to do formal proofs of Haskell programs ?
2025-08-27 04:06:03 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-08-27 04:06:50 +0200 <geekosaur> Axman6: have you considered using FFI to an existing one?
2025-08-27 04:06:58 +0200speedycoder(uid644440@user/speedycoder) speedycoder
2025-08-27 04:07:57 +0200 <haskellbridge> <Axman6> That feels overkill for this particular problem, I’m just trying to add a new colour space to the Color package.
2025-08-27 04:09:34 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-08-27 04:11:58 +0200 <Leary> Axman6: https://hackage.haskell.org/package/numeric-extras-0.1/docs/Numeric-Extras.html#v:cbrt
2025-08-27 04:12:02 +0200crazazy(~crazazy@tilde.town) (Ping timeout: 256 seconds)
2025-08-27 04:13:08 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-08-27 04:13:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 04:18:11 +0200haskellman(~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422) (Ping timeout: 250 seconds)
2025-08-27 04:18:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-08-27 04:18:32 +0200tessier(~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 256 seconds)
2025-08-27 04:20:17 +0200tessier(~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) tessier
2025-08-27 04:22:48 +0200itaipu(~itaipu@168.121.97.28) (Ping timeout: 248 seconds)
2025-08-27 04:25:39 +0200cyphase(~cyphase@user/cyphase) (Ping timeout: 258 seconds)
2025-08-27 04:27:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 04:28:00 +0200ec(~ec@gateway/tor-sasl/ec) (Remote host closed the connection)
2025-08-27 04:28:21 +0200ec(~ec@gateway/tor-sasl/ec) ec
2025-08-27 04:31:17 +0200haskellman(~haskellma@2a01:e0a:16a:7710:8e5d:8bc6:7f23:6d6d)
2025-08-27 04:31:47 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds)
2025-08-27 04:32:29 +0200 <haskellman> Hello everyone, Which prover should I choose to prove my Haskell program. Why can't Ijust import Haskell into the prover and have that as part of the compilation step ? How efficient is the code produced ? Thank you.
2025-08-27 04:34:30 +0200pabs3(~pabs3@user/pabs3) pabs3
2025-08-27 04:38:40 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds)
2025-08-27 04:42:32 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 04:47:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-08-27 04:56:19 +0200shapr(~user@130.44.148.32) (Ping timeout: 258 seconds)
2025-08-27 04:56:39 +0200 <geekosaur> there are no provers designed to take unmodified Haskell code. the closest you get is to modify Haskell code for Agda or Idris.
2025-08-27 04:57:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-27 04:59:34 +0200 <geekosaur> (dons modified XMonad.StackSet for Agda and proved it there, although I'm not sure if that's still online anywhere (I'm not finding it on a quick check)
2025-08-27 05:00:16 +0200 <geekosaur> (Wouter Swierstra also reimplemented it in Rocq to formally verify it, but that's a much larger transformation than Idris would be)
2025-08-27 05:00:45 +0200 <geekosaur> https://webspace.science.uu.nl/~swier004/publications/2012-haskell.pdf
2025-08-27 05:02:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)