Logs: liberachat/#haskell
| 2025-08-27 01:28:48 | × | fgarcia quits (~lei@user/fgarcia) (Read error: Connection reset by peer) |
| 2025-08-27 01:28:53 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-08-27 01:28:57 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 256 seconds) |
| 2025-08-27 01:29:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-27 01:34:18 | → | fgarcia joins (~lei@user/fgarcia) |
| 2025-08-27 01:35:24 | → | itaipu joins (~itaipu@168.121.97.28) |
| 2025-08-27 01:36:15 | × | fgarcia quits (~lei@user/fgarcia) (Read error: Connection reset by peer) |
| 2025-08-27 01:36:39 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-08-27 01:40:14 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2025-08-27 01:40:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 01:40:18 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 256 seconds) |
| 2025-08-27 01:41:44 | → | cyphase joins (~cyphase@user/cyphase) |
| 2025-08-27 01:41:49 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-08-27 01:42:52 | → | fgarcia joins (~lei@user/fgarcia) |
| 2025-08-27 01:43:03 | × | hakutaku quits (~textual@chen.yukari.eu.org) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2025-08-27 01:43:44 | → | hakutaku joins (~textual@chen.yukari.eu.org) |
| 2025-08-27 01:43:44 | × | fgarcia quits (~lei@user/fgarcia) (Read error: Connection reset by peer) |
| 2025-08-27 01:44:38 | → | fgarcia joins (~lei@user/fgarcia) |
| 2025-08-27 01:46:18 | trickard_ | is now known as trickard |
| 2025-08-27 01:47:02 | × | fgarcia quits (~lei@user/fgarcia) (Read error: Connection reset by peer) |
| 2025-08-27 01:47:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 01:53:59 | → | fgarcia joins (~lei@user/fgarcia) |
| 2025-08-27 01:54:53 | <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 01:58:22 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 02:01:12 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 272 seconds) |
| 2025-08-27 02:02:29 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2025-08-27 02:03:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 02:04:02 | → | haskellman joins (~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422) |
| 2025-08-27 02:04:08 | × | pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 248 seconds) |
| 2025-08-27 02:04:23 | <haskellman> | Hello, how to do formal proofs of Haskell programs ? |
| 2025-08-27 02:06:03 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-08-27 02:06:50 | <geekosaur> | Axman6: have you considered using FFI to an existing one? |
| 2025-08-27 02:06:58 | → | speedycoder joins (uid644440@user/speedycoder) |
| 2025-08-27 02:07:57 | <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 02:09:34 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2025-08-27 02:11:58 | <Leary> | Axman6: https://hackage.haskell.org/package/numeric-extras-0.1/docs/Numeric-Extras.html#v:cbrt |
| 2025-08-27 02:12:02 | × | crazazy quits (~crazazy@tilde.town) (Ping timeout: 256 seconds) |
| 2025-08-27 02:13:08 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2025-08-27 02:13:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 02:18:11 | × | haskellman quits (~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422) (Ping timeout: 250 seconds) |
| 2025-08-27 02:18:15 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-27 02:18:32 | × | tessier quits (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 256 seconds) |
| 2025-08-27 02:20:17 | → | tessier joins (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 2025-08-27 02:22:48 | × | itaipu quits (~itaipu@168.121.97.28) (Ping timeout: 248 seconds) |
| 2025-08-27 02:25:39 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 258 seconds) |
| 2025-08-27 02:27:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 02:28:00 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2025-08-27 02:28:21 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2025-08-27 02:31:17 | → | haskellman joins (~haskellma@2a01:e0a:16a:7710:8e5d:8bc6:7f23:6d6d) |
| 2025-08-27 02:31:47 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 02:32:29 | <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 02:34:30 | → | pabs3 joins (~pabs3@user/pabs3) |
| 2025-08-27 02:38:40 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-08-27 02:42:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 02:47:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-27 02:56:19 | × | shapr quits (~user@130.44.148.32) (Ping timeout: 258 seconds) |
| 2025-08-27 02:56:39 | <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 02:57:56 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 02:59:34 | <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 03:00:16 | <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 03:00:45 | <geekosaur> | https://webspace.science.uu.nl/~swier004/publications/2012-haskell.pdf |
| 2025-08-27 03:02:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 03:07:57 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-08-27 03:10:07 | → | xff0x_ joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-08-27 03:11:06 | → | poscat joins (~poscat@user/poscat) |
| 2025-08-27 03:11:20 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 2025-08-27 03:13:18 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 03:17:46 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 03:26:08 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
| 2025-08-27 03:26:48 | × | Frostillicus quits (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 2025-08-27 03:28:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 03:29:24 | → | aforemny joins (~aforemny@2001:9e8:6cc0:e200:af3c:2230:d3c7:66cc) |
| 2025-08-27 03:29:48 | × | aforemny_ quits (~aforemny@2001:9e8:6ce0:b400:b37:e7d1:7c56:28e9) (Ping timeout: 244 seconds) |
| 2025-08-27 03:31:51 | × | haskellman quits (~haskellma@2a01:e0a:16a:7710:8e5d:8bc6:7f23:6d6d) (Ping timeout: 250 seconds) |
| 2025-08-27 03:35:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 03:38:25 | xff0x_ | is now known as xff0x |
| 2025-08-27 03:38:32 | → | vetkat9 joins (~vetkat@user/vetkat) |
| 2025-08-27 03:40:01 | × | vetkat quits (~vetkat@user/vetkat) (Ping timeout: 258 seconds) |
| 2025-08-27 03:40:01 | vetkat9 | is now known as vetkat |
| 2025-08-27 03:40:43 | × | sp1ff quits (~user@c-24-21-190-184.hsd1.wa.comcast.net) (Ping timeout: 256 seconds) |
| 2025-08-27 03:41:04 | → | sp1ff joins (~user@c-24-21-190-184.hsd1.wa.comcast.net) |
| 2025-08-27 03:41:06 | × | catties quits (~catties@user/meow/catties) (Server closed connection) |
| 2025-08-27 03:41:07 | → | itaipu joins (~itaipu@168.121.97.28) |
| 2025-08-27 03:41:26 | → | catties joins (~catties@user/meow/catties) |
| 2025-08-27 03:43:40 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 2025-08-27 03:46:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 03:51:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-27 03:54:54 | nitrix_ | is now known as nitrix |
| 2025-08-27 03:55:47 | → | cyphase joins (~cyphase@user/cyphase) |
| 2025-08-27 03:58:15 | → | crazazy joins (~crazazy@tilde.town) |
| 2025-08-27 04:00:24 | × | noctux quits (~noctux@user/noctux) (Server closed connection) |
| 2025-08-27 04:00:33 | → | noctux joins (~noctux@user/noctux) |
| 2025-08-27 04:01:29 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 258 seconds) |
| 2025-08-27 04:12:42 | → | visilii joins (~visilii@213.24.125.93) |
| 2025-08-27 04:13:44 | × | segfaultfizzbuzz quits (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) (Ping timeout: 248 seconds) |
| 2025-08-27 04:23:42 | × | crazazy quits (~crazazy@tilde.town) (Quit: WeeChat 4.6.3) |
| 2025-08-27 04:28:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-27 04:32:51 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 04:32:55 | × | itaipu quits (~itaipu@168.121.97.28) (Ping timeout: 258 seconds) |
| 2025-08-27 04:41:40 | → | segfaultfizzbuzz joins (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
All times are in UTC.