Newest at the top
| 2025-08-27 05:17:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 05:13:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 05:11:20 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 248 seconds) |
| 2025-08-27 05:11:06 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-08-27 05:10:07 +0200 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-08-27 05:07:57 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-08-27 05:02:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 05:00:45 +0200 | <geekosaur> | https://webspace.science.uu.nl/~swier004/publications/2012-haskell.pdf |
| 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 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 04:57:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 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:56:19 +0200 | shapr | (~user@130.44.148.32) (Ping timeout: 258 seconds) |
| 2025-08-27 04:47:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-27 04:42:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 04:38:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-08-27 04:34:30 +0200 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 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:31:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 04:31:17 +0200 | haskellman | (~haskellma@2a01:e0a:16a:7710:8e5d:8bc6:7f23:6d6d) |
| 2025-08-27 04:28:21 +0200 | ec | (~ec@gateway/tor-sasl/ec) ec |
| 2025-08-27 04:28:00 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2025-08-27 04:27:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 04:25:39 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 258 seconds) |
| 2025-08-27 04:22:48 +0200 | itaipu | (~itaipu@168.121.97.28) (Ping timeout: 248 seconds) |
| 2025-08-27 04:20:17 +0200 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) tessier |
| 2025-08-27 04:18:32 +0200 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 256 seconds) |
| 2025-08-27 04:18:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-27 04:18:11 +0200 | haskellman | (~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422) (Ping timeout: 250 seconds) |
| 2025-08-27 04:13:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 04:13:08 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-08-27 04:12:02 +0200 | crazazy | (~crazazy@tilde.town) (Ping timeout: 256 seconds) |
| 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:09:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 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:06:58 +0200 | speedycoder | (uid644440@user/speedycoder) speedycoder |
| 2025-08-27 04:06:50 +0200 | <geekosaur> | Axman6: have you considered using FFI to an existing one? |
| 2025-08-27 04:06:03 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-08-27 04:04:23 +0200 | <haskellman> | Hello, how to do formal proofs of Haskell programs ? |
| 2025-08-27 04:04:08 +0200 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 248 seconds) |
| 2025-08-27 04:04:02 +0200 | haskellman | (~haskellma@2a01:e0a:16a:7710:fd55:5b5c:cc6f:c422) |
| 2025-08-27 04:03:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-08-27 04:02:29 +0200 | ec | (~ec@gateway/tor-sasl/ec) ec |
| 2025-08-27 04:01:12 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 272 seconds) |
| 2025-08-27 03:58:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 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:53:59 +0200 | fgarcia | (~lei@user/fgarcia) fgarcia |
| 2025-08-27 03:47:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 03:47:02 +0200 | fgarcia | (~lei@user/fgarcia) (Read error: Connection reset by peer) |
| 2025-08-27 03:46:18 +0200 | trickard_ | trickard |