Newest at the top
| 2026-02-04 22:46:29 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-04 22:46:19 +0100 | cyphase | (~cyphase@user/cyphase) (Ping timeout: 265 seconds) |
| 2026-02-04 22:44:31 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 246 seconds) |
| 2026-02-04 22:41:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-04 22:39:51 +0100 | michalz | (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2026-02-04 22:39:48 +0100 | <monochrom> | Well, in the limit, minimize both verification by humans and synthesis by humans. We're getting there! |
| 2026-02-04 22:38:51 +0100 | <monochrom> | Industry wants to minimize proofs-by-humans. So they will take automated checks, or more recently, proofs-by-AI. |
| 2026-02-04 22:38:02 +0100 | Googulator | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) |
| 2026-02-04 22:37:46 +0100 | Googulator | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-04 22:31:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-04 22:27:37 +0100 | <jreicher> | mesaoptimizer: I don't do Haskell heavily in Emacs, but based on my experience with other languages and what I'm seeing out there I would strongly recommend eglot, regardless of the major mode you choose, and then do your own comparison of haskell-mode vs haskell-ts-mode. (My hunch is the latter is better.) |
| 2026-02-04 22:25:51 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-04 22:22:56 +0100 | acidjnk | (~acidjnk@p200300d6e700e57835d41376842fa308.dip0.t-ipconnect.de) acidjnk |
| 2026-02-04 22:22:33 +0100 | acidjnk | (~acidjnk@p200300d6e700e57835d41376842fa308.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2026-02-04 22:16:31 +0100 | AlexZenon | (~alzenon@85.174.181.199) (Ping timeout: 240 seconds) |
| 2026-02-04 22:15:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-04 22:14:23 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-04 22:14:13 +0100 | AlexZenon_2 | (~alzenon@85.174.181.199) |
| 2026-02-04 22:14:10 +0100 | trickard | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-04 22:12:13 +0100 | AlexZenon_2 | (~alzenon@85.174.181.199) (Ping timeout: 260 seconds) |
| 2026-02-04 22:12:11 +0100 | AlexZenon | (~alzenon@85.174.181.199) |
| 2026-02-04 22:10:28 +0100 | AlexZenon | (~alzenon@85.174.181.199) (Ping timeout: 260 seconds) |
| 2026-02-04 22:10:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-04 22:07:47 +0100 | AlexZenon_2 | (~alzenon@85.174.181.199) |
| 2026-02-04 22:05:26 +0100 | AlexZenon | (~alzenon@85.174.181.199) |
| 2026-02-04 22:04:42 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2026-02-04 22:02:34 +0100 | AlexZenon | (~alzenon@85.174.181.199) (Ping timeout: 256 seconds) |
| 2026-02-04 21:58:51 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-04 21:58:11 +0100 | housemate | (~housemate@202.7.248.67) housemate |
| 2026-02-04 21:54:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-04 21:44:56 +0100 | Googulator2 | Googulator |
| 2026-02-04 21:44:15 +0100 | <tomsmeding> | perhaps that's overly reductive. But maybe the same holds for proof systems in general; industry use of formal methods seems to saturate around the point of model checking |
| 2026-02-04 21:43:13 +0100 | <tomsmeding> | systems for formalising mathematics are not very attractive to industry, I'd wager |
| 2026-02-04 21:43:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-04 21:36:14 +0100 | vidak | (~vidak@2407:e400:7800:2c01:d0be:76f8:cc84:bd4a) (Ping timeout: 265 seconds) |
| 2026-02-04 21:36:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-04 21:28:29 +0100 | Googulator27 | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-04 21:28:25 +0100 | Googulator2 | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) |
| 2026-02-04 21:25:59 +0100 | <__monty__> | Isn't Lean academic? |
| 2026-02-04 21:12:56 +0100 | tromp | (~textual@2001:1c00:3487:1b00:10a6:5d4a:b26:4065) |
| 2026-02-04 21:11:47 +0100 | spew | (~spew@user/spew) (Read error: Connection reset by peer) |
| 2026-02-04 21:02:22 +0100 | kuribas | (~user@2a02-1810-2825-6000-16d8-7b7e-1bcd-b36.ip6.access.telenet.be) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2026-02-04 21:01:20 +0100 | polykernel | (~polykerne@user/polykernel) polykernel |
| 2026-02-04 20:58:35 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2026-02-04 20:57:37 +0100 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 264 seconds) |
| 2026-02-04 20:53:09 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-02-04 20:51:15 +0100 | polykernel | (~polykerne@user/polykernel) (Remote host closed the connection) |
| 2026-02-04 20:50:03 +0100 | spew | (~spew@user/spew) spew |
| 2026-02-04 20:49:40 +0100 | Googulator27 | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) |
| 2026-02-04 20:49:25 +0100 | Googulator27 | (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) (Quit: Client closed) |