Newest at the top
| 2025-08-27 06:01:29 +0200 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 258 seconds) |
| 2025-08-27 06:00:33 +0200 | noctux | (~noctux@user/noctux) noctux |
| 2025-08-27 06:00:24 +0200 | noctux | (~noctux@user/noctux) (Server closed connection) |
| 2025-08-27 05:58:15 +0200 | crazazy | (~crazazy@tilde.town) crazazy |
| 2025-08-27 05:55:47 +0200 | cyphase | (~cyphase@user/cyphase) cyphase |
| 2025-08-27 05:54:54 +0200 | nitrix_ | nitrix |
| 2025-08-27 05:51:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-27 05:46:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 05:43:40 +0200 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 245 seconds) |
| 2025-08-27 05:41:26 +0200 | catties | (~catties@user/meow/catties) catties |
| 2025-08-27 05:41:07 +0200 | itaipu | (~itaipu@168.121.97.28) itaipu |
| 2025-08-27 05:41:06 +0200 | catties | (~catties@user/meow/catties) (Server closed connection) |
| 2025-08-27 05:41:04 +0200 | sp1ff | (~user@c-24-21-190-184.hsd1.wa.comcast.net) sp1ff |
| 2025-08-27 05:40:43 +0200 | sp1ff | (~user@c-24-21-190-184.hsd1.wa.comcast.net) (Ping timeout: 256 seconds) |
| 2025-08-27 05:40:01 +0200 | vetkat9 | vetkat |
| 2025-08-27 05:40:01 +0200 | vetkat | (~vetkat@user/vetkat) (Ping timeout: 258 seconds) |
| 2025-08-27 05:38:32 +0200 | vetkat9 | (~vetkat@user/vetkat) vetkat |
| 2025-08-27 05:38:25 +0200 | xff0x_ | xff0x |
| 2025-08-27 05:35:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 258 seconds) |
| 2025-08-27 05:31:51 +0200 | haskellman | (~haskellma@2a01:e0a:16a:7710:8e5d:8bc6:7f23:6d6d) (Ping timeout: 250 seconds) |
| 2025-08-27 05:29:48 +0200 | aforemny_ | (~aforemny@2001:9e8:6ce0:b400:b37:e7d1:7c56:28e9) (Ping timeout: 244 seconds) |
| 2025-08-27 05:29:24 +0200 | aforemny | (~aforemny@2001:9e8:6cc0:e200:af3c:2230:d3c7:66cc) aforemny |
| 2025-08-27 05:28:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-27 05:26:48 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Ping timeout: 248 seconds) |
| 2025-08-27 05:26:08 +0200 | segfaultfizzbuzz | (~segfaultf@23-93-74-222.fiber.dynamic.sonic.net) |
| 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) |