Logs: liberachat/#haskell
| 2026-02-04 19:57:37 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 264 seconds) |
| 2026-02-04 19:58:35 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 2026-02-04 20:01:20 | → | polykernel joins (~polykerne@user/polykernel) |
| 2026-02-04 20:02:22 | × | kuribas quits (~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 20:11:47 | × | spew quits (~spew@user/spew) (Read error: Connection reset by peer) |
| 2026-02-04 20:12:56 | → | tromp joins (~textual@2001:1c00:3487:1b00:10a6:5d4a:b26:4065) |
| 2026-02-04 20:25:59 | <__monty__> | Isn't Lean academic? |
| 2026-02-04 20:28:25 | → | Googulator2 joins (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) |
| 2026-02-04 20:28:29 | × | Googulator27 quits (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-04 20:36:13 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 20:36:14 | × | vidak quits (~vidak@2407:e400:7800:2c01:d0be:76f8:cc84:bd4a) (Ping timeout: 265 seconds) |
| 2026-02-04 20:43:00 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-04 20:43:13 | <tomsmeding> | systems for formalising mathematics are not very attractive to industry, I'd wager |
| 2026-02-04 20:44:15 | <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 20:44:56 | Googulator2 | is now known as Googulator |
| 2026-02-04 20:54:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 20:58:11 | → | housemate joins (~housemate@202.7.248.67) |
| 2026-02-04 20:58:51 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-04 21:02:34 | × | AlexZenon quits (~alzenon@85.174.181.199) (Ping timeout: 256 seconds) |
| 2026-02-04 21:04:42 | → | pavonia joins (~user@user/siracusa) |
| 2026-02-04 21:05:26 | → | AlexZenon joins (~alzenon@85.174.181.199) |
| 2026-02-04 21:07:47 | → | AlexZenon_2 joins (~alzenon@85.174.181.199) |
| 2026-02-04 21:10:05 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 21:10:28 | × | AlexZenon quits (~alzenon@85.174.181.199) (Ping timeout: 260 seconds) |
| 2026-02-04 21:12:11 | → | AlexZenon joins (~alzenon@85.174.181.199) |
| 2026-02-04 21:12:13 | × | AlexZenon_2 quits (~alzenon@85.174.181.199) (Ping timeout: 260 seconds) |
| 2026-02-04 21:14:10 | × | trickard quits (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-04 21:14:13 | → | AlexZenon_2 joins (~alzenon@85.174.181.199) |
| 2026-02-04 21:14:23 | → | trickard_ joins (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-04 21:15:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-04 21:16:31 | × | AlexZenon quits (~alzenon@85.174.181.199) (Ping timeout: 240 seconds) |
| 2026-02-04 21:22:33 | × | acidjnk quits (~acidjnk@p200300d6e700e57835d41376842fa308.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2026-02-04 21:22:56 | → | acidjnk joins (~acidjnk@p200300d6e700e57835d41376842fa308.dip0.t-ipconnect.de) |
| 2026-02-04 21:25:51 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 21:27:37 | <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 21:31:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-04 21:37:46 | × | Googulator quits (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-04 21:38:02 | → | Googulator joins (~Googulato@2a01-036d-0106-216f-0081-f2ad-9e0f-9d89.pool6.digikabel.hu) |
| 2026-02-04 21:38:51 | <monochrom> | Industry wants to minimize proofs-by-humans. So they will take automated checks, or more recently, proofs-by-AI. |
| 2026-02-04 21:39:48 | <monochrom> | Well, in the limit, minimize both verification by humans and synthesis by humans. We're getting there! |
| 2026-02-04 21:39:51 | × | michalz quits (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2026-02-04 21:41:40 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 21:44:31 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 246 seconds) |
| 2026-02-04 21:46:19 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 265 seconds) |
| 2026-02-04 21:46:29 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-04 21:48:43 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2026-02-04 21:48:53 | × | tromp quits (~textual@2001:1c00:3487:1b00:10a6:5d4a:b26:4065) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-02-04 21:51:21 | <jreicher> | Verification by humans will never completely go away. When people die, there's general agreement the software might have done the wrong thing. |
| 2026-02-04 21:51:56 | <jreicher> | Better not to test in prod though, of course. |
| 2026-02-04 21:52:19 | × | hakutaku quits (~textual@user/hakutaku) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2026-02-04 21:52:46 | → | hakutaku joins (~textual@user/hakutaku) |
| 2026-02-04 21:52:46 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2026-02-04 21:54:37 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-02-04 21:55:54 | → | tromp joins (~textual@2001:1c00:3487:1b00:10a6:5d4a:b26:4065) |
| 2026-02-04 21:57:25 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 22:02:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-04 22:05:05 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2026-02-04 22:06:47 | <gentauro> | with regard to LEAN, I like the following explanation from Charles Hoskinson: https://www.youtube.com/watch?v=3snIzhjqsk0 (academic papers tend to loose insights, so by providing a more formal framework, we might have better insights) |
| 2026-02-04 22:14:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 22:18:59 | × | xff0x quits (~xff0x@2405:6580:b080:900:5e48:b86:53c8:1c87) (Quit: xff0x) |
| 2026-02-04 22:21:20 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-04 22:21:50 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-02-04 22:29:32 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2026-02-04 22:29:37 | → | chexum_ joins (~quassel@gateway/tor-sasl/chexum) |
| 2026-02-04 22:32:45 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 22:34:49 | <EvanR> | jreicher, sure... blame the computer! |
| 2026-02-04 22:35:36 | <EvanR> | technology, industrialization absolving people of accountability |
| 2026-02-04 22:37:22 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-04 22:39:48 | <jreicher> | EvanR: I know you're joking, but in all seriousness I "lecture" to every non-techy I meet that when a bug hits it's not a computer malfunction. The computer did exactly what it was told to do. It's the developers who malfunctioned. |
| 2026-02-04 22:41:15 | <EvanR> | (except for surface level consumer hardware does experience random errors for reasons... though that's just another instance of the same point) |
| 2026-02-04 22:42:45 | <EvanR> | one of these esolangs has your code devolving as it runs, due to "entropy"... annoying until you accept this is happening to your real computer all the time xD |
| 2026-02-04 22:43:16 | <EvanR> | at a much slower pace |
| 2026-02-04 22:43:37 | <jreicher> | Yeah, this is specific to "bugs" |
| 2026-02-04 22:45:54 | × | skum quits (~skum@user/skum) (Quit: WeeChat 4.8.1) |
| 2026-02-04 22:46:29 | <EvanR> | this code is provided without any warranty or even an implied warranty of merchantability or fitness for a particular purpose! |
| 2026-02-04 22:48:18 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 22:48:48 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2026-02-04 22:52:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-04 22:54:03 | → | skum joins (~skum@user/skum) |
| 2026-02-04 22:56:22 | → | xff0x joins (~xff0x@2405:6580:b080:900:d171:1c19:51a5:d6b5) |
| 2026-02-04 23:01:34 | × | tromp quits (~textual@2001:1c00:3487:1b00:10a6:5d4a:b26:4065) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-02-04 23:04:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 23:08:56 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-04 23:15:24 | → | mange joins (~mange@user/mange) |
| 2026-02-04 23:18:37 | × | paddymahoney quits (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Remote host closed the connection) |
| 2026-02-04 23:19:53 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 23:24:13 | → | paddymahoney joins (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) |
| 2026-02-04 23:24:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-02-04 23:28:55 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 2026-02-04 23:33:40 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 23:38:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-02-04 23:40:50 | <haskellbridge> | <loonycyborg> There still are actual malfunctions out there, like faulty ram modules that flip some bits. |
| 2026-02-04 23:41:26 | <haskellbridge> | <loonycyborg> good luck figuring out what is because of such a malfunction and what comes from programmer brainfarts :P |
| 2026-02-04 23:44:07 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-02-04 23:49:23 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-04 23:50:38 | <EvanR> | not just faulty ram, unless it's by definition, even space grade chips will be giving a rating in terms of probability |
| 2026-02-04 23:51:48 | <lantti> | isn't it still a programmers decision if it is acceptable that such malfunctions cause a program to fail (considering severity and probability etc.)? |
| 2026-02-04 23:52:39 | <lantti> | if it is not then the programmer must take that into consideration and have reduncancy and whatnot |
| 2026-02-04 23:52:43 | <EvanR> | that's the esolang I was talking about |
| 2026-02-04 23:52:55 | <jreicher> | I wish my workplace tested with chaosmonkey |
All times are in UTC.