| 2024-12-04 00:00:39 +0100 | alp | (~alp@2001:861:8ca0:4940:e76a:7d36:8adc:27e3) (Remote host closed the connection) |
| 2024-12-04 00:00:57 +0100 | alp | (~alp@2001:861:8ca0:4940:2134:167a:303d:5617) |
| 2024-12-04 00:02:20 +0100 | alp | (~alp@2001:861:8ca0:4940:2134:167a:303d:5617) (Remote host closed the connection) |
| 2024-12-04 00:02:37 +0100 | alp | (~alp@2001:861:8ca0:4940:32d1:b188:aa8d:80b0) |
| 2024-12-04 00:04:01 +0100 | alp | (~alp@2001:861:8ca0:4940:32d1:b188:aa8d:80b0) (Remote host closed the connection) |
| 2024-12-04 00:04:18 +0100 | alp | (~alp@2001:861:8ca0:4940:53e6:2ee0:3c96:ba17) |
| 2024-12-04 00:05:42 +0100 | alp | (~alp@2001:861:8ca0:4940:53e6:2ee0:3c96:ba17) (Remote host closed the connection) |
| 2024-12-04 00:05:59 +0100 | alp | (~alp@2001:861:8ca0:4940:8cdb:a56:d144:a524) |
| 2024-12-04 00:07:41 +0100 | alp_ | (~alp@2001:861:8ca0:4940:b7d8:58c7:6786:7d57) |
| 2024-12-04 00:09:24 +0100 | alp__ | (~alp@2001:861:8ca0:4940:19e:b817:16a3:105c) |
| 2024-12-04 00:10:45 +0100 | alp | (~alp@2001:861:8ca0:4940:8cdb:a56:d144:a524) (Ping timeout: 248 seconds) |
| 2024-12-04 00:10:47 +0100 | alp__ | (~alp@2001:861:8ca0:4940:19e:b817:16a3:105c) (Remote host closed the connection) |
| 2024-12-04 00:11:04 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e5c2:6c92:e493:e6dd) |
| 2024-12-04 00:12:29 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e5c2:6c92:e493:e6dd) (Remote host closed the connection) |
| 2024-12-04 00:12:46 +0100 | alp__ | (~alp@2001:861:8ca0:4940:8cf8:84fd:c29d:ded4) |
| 2024-12-04 00:12:53 +0100 | alp_ | (~alp@2001:861:8ca0:4940:b7d8:58c7:6786:7d57) (Ping timeout: 248 seconds) |
| 2024-12-04 00:14:12 +0100 | alp__ | (~alp@2001:861:8ca0:4940:8cf8:84fd:c29d:ded4) (Remote host closed the connection) |
| 2024-12-04 00:14:28 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e711:d17b:85ba:6e68) |
| 2024-12-04 00:15:54 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e711:d17b:85ba:6e68) (Remote host closed the connection) |
| 2024-12-04 00:16:11 +0100 | alp__ | (~alp@2001:861:8ca0:4940:da39:ecb7:24a3:fa7c) |
| 2024-12-04 00:17:36 +0100 | alp__ | (~alp@2001:861:8ca0:4940:da39:ecb7:24a3:fa7c) (Remote host closed the connection) |
| 2024-12-04 00:17:53 +0100 | alp__ | (~alp@2001:861:8ca0:4940:248:7c82:2e7e:d482) |
| 2024-12-04 00:19:18 +0100 | alp__ | (~alp@2001:861:8ca0:4940:248:7c82:2e7e:d482) (Remote host closed the connection) |
| 2024-12-04 00:19:35 +0100 | alp__ | (~alp@2001:861:8ca0:4940:6255:bcf2:af03:3641) |
| 2024-12-04 00:21:00 +0100 | alp__ | (~alp@2001:861:8ca0:4940:6255:bcf2:af03:3641) (Remote host closed the connection) |
| 2024-12-04 00:21:17 +0100 | alp__ | (~alp@2001:861:8ca0:4940:487b:94b7:43cf:3ccc) |
| 2024-12-04 00:22:42 +0100 | alp__ | (~alp@2001:861:8ca0:4940:487b:94b7:43cf:3ccc) (Remote host closed the connection) |
| 2024-12-04 00:22:59 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e89d:a86a:2e60:67c5) |
| 2024-12-04 00:24:25 +0100 | alp__ | (~alp@2001:861:8ca0:4940:e89d:a86a:2e60:67c5) (Remote host closed the connection) |
| 2024-12-04 00:24:42 +0100 | alp__ | (~alp@2001:861:8ca0:4940:5270:bdae:7548:3af1) |
| 2024-12-04 00:25:24 +0100 | catman | (~catman@user/catman) (Ping timeout: 276 seconds) |
| 2024-12-04 00:26:06 +0100 | alp__ | (~alp@2001:861:8ca0:4940:5270:bdae:7548:3af1) (Remote host closed the connection) |
| 2024-12-04 00:26:23 +0100 | alp__ | (~alp@2001:861:8ca0:4940:4cea:f7a:2dd7:2a8) |
| 2024-12-04 00:27:07 +0100 | catman | (~catman@user/catman) catman |
| 2024-12-04 00:27:48 +0100 | alp__ | (~alp@2001:861:8ca0:4940:4cea:f7a:2dd7:2a8) (Remote host closed the connection) |
| 2024-12-04 00:28:05 +0100 | alp__ | (~alp@2001:861:8ca0:4940:c06:15fd:dd93:fa63) |
| 2024-12-04 00:29:30 +0100 | alp__ | (~alp@2001:861:8ca0:4940:c06:15fd:dd93:fa63) (Remote host closed the connection) |
| 2024-12-04 00:29:47 +0100 | alp__ | (~alp@2001:861:8ca0:4940:1d46:1aa0:4e7f:b2f9) |
| 2024-12-04 00:31:30 +0100 | alp_ | (~alp@2001:861:8ca0:4940:73f1:fc81:eaca:26f6) |
| 2024-12-04 00:32:55 +0100 | alp_ | (~alp@2001:861:8ca0:4940:73f1:fc81:eaca:26f6) (Remote host closed the connection) |
| 2024-12-04 00:33:12 +0100 | alp_ | (~alp@2001:861:8ca0:4940:7e12:ac14:b600:1a67) |
| 2024-12-04 00:34:33 +0100 | alp__ | (~alp@2001:861:8ca0:4940:1d46:1aa0:4e7f:b2f9) (Ping timeout: 246 seconds) |
| 2024-12-04 00:34:37 +0100 | alp_ | (~alp@2001:861:8ca0:4940:7e12:ac14:b600:1a67) (Remote host closed the connection) |
| 2024-12-04 00:34:53 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8a72:4fa4:8dbc:5fb1) |
| 2024-12-04 00:36:19 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8a72:4fa4:8dbc:5fb1) (Remote host closed the connection) |
| 2024-12-04 00:36:36 +0100 | alp_ | (~alp@2001:861:8ca0:4940:e2d0:740d:3023:9109) |
| 2024-12-04 00:38:01 +0100 | alp_ | (~alp@2001:861:8ca0:4940:e2d0:740d:3023:9109) (Remote host closed the connection) |
| 2024-12-04 00:38:18 +0100 | alp_ | (~alp@2001:861:8ca0:4940:bc0e:2aee:6a22:2d20) |
| 2024-12-04 00:39:43 +0100 | alp_ | (~alp@2001:861:8ca0:4940:bc0e:2aee:6a22:2d20) (Remote host closed the connection) |
| 2024-12-04 00:40:00 +0100 | alp_ | (~alp@2001:861:8ca0:4940:658:5d41:1e17:177a) |
| 2024-12-04 00:41:44 +0100 | alp__ | (~alp@2001:861:8ca0:4940:f868:e2da:2313:3292) |
| 2024-12-04 00:43:07 +0100 | alp__ | (~alp@2001:861:8ca0:4940:f868:e2da:2313:3292) (Remote host closed the connection) |
| 2024-12-04 00:43:25 +0100 | alp__ | (~alp@2001:861:8ca0:4940:a1d4:8f5:ea39:48) |
| 2024-12-04 00:44:42 +0100 | alp_ | (~alp@2001:861:8ca0:4940:658:5d41:1e17:177a) (Ping timeout: 246 seconds) |
| 2024-12-04 00:45:07 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8329:3732:b124:24b7) |
| 2024-12-04 00:46:31 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8329:3732:b124:24b7) (Remote host closed the connection) |
| 2024-12-04 00:46:49 +0100 | alp_ | (~alp@2001:861:8ca0:4940:6376:2500:12a5:17ce) |
| 2024-12-04 00:48:13 +0100 | alp_ | (~alp@2001:861:8ca0:4940:6376:2500:12a5:17ce) (Remote host closed the connection) |
| 2024-12-04 00:48:32 +0100 | alp_ | (~alp@2001:861:8ca0:4940:6e86:45d3:7da3:dca9) |
| 2024-12-04 00:48:50 +0100 | alp__ | (~alp@2001:861:8ca0:4940:a1d4:8f5:ea39:48) (Ping timeout: 260 seconds) |
| 2024-12-04 00:49:56 +0100 | alp_ | (~alp@2001:861:8ca0:4940:6e86:45d3:7da3:dca9) (Remote host closed the connection) |
| 2024-12-04 00:50:13 +0100 | alp_ | (~alp@2001:861:8ca0:4940:787f:767d:4686:fe80) |
| 2024-12-04 00:51:37 +0100 | alp_ | (~alp@2001:861:8ca0:4940:787f:767d:4686:fe80) (Remote host closed the connection) |
| 2024-12-04 00:51:56 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8598:7fdf:3873:87a8) |
| 2024-12-04 00:53:20 +0100 | alp_ | (~alp@2001:861:8ca0:4940:8598:7fdf:3873:87a8) (Remote host closed the connection) |
| 2024-12-04 00:53:37 +0100 | alp_ | (~alp@2001:861:8ca0:4940:32ee:f693:b590:f66c) |
| 2024-12-04 00:55:02 +0100 | alp_ | (~alp@2001:861:8ca0:4940:32ee:f693:b590:f66c) (Remote host closed the connection) |
| 2024-12-04 00:55:20 +0100 | alp_ | (~alp@2001:861:8ca0:4940:2099:9745:f1c7:8705) |
| 2024-12-04 00:56:44 +0100 | alp_ | (~alp@2001:861:8ca0:4940:2099:9745:f1c7:8705) (Remote host closed the connection) |
| 2024-12-04 00:57:02 +0100 | alp_ | (~alp@2001:861:8ca0:4940:ab2:c635:31cc:2871) |
| 2024-12-04 00:58:26 +0100 | alp_ | (~alp@2001:861:8ca0:4940:ab2:c635:31cc:2871) (Remote host closed the connection) |
| 2024-12-04 00:58:43 +0100 | alp_ | (~alp@2001:861:8ca0:4940:5aee:7e5d:1206:a620) |
| 2024-12-04 01:00:08 +0100 | alp_ | (~alp@2001:861:8ca0:4940:5aee:7e5d:1206:a620) (Remote host closed the connection) |
| 2024-12-04 01:00:25 +0100 | alp_ | (~alp@2001:861:8ca0:4940:a886:2477:d10a:75c1) |
| 2024-12-04 01:02:09 +0100 | alp__ | (~alp@128-79-174-146.hfc.dyn.abo.bbox.fr) |
| 2024-12-04 01:05:13 +0100 | alp_ | (~alp@2001:861:8ca0:4940:a886:2477:d10a:75c1) (Ping timeout: 252 seconds) |
| 2024-12-04 01:34:51 +0100 | OftenFaded | (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 2024-12-04 02:04:36 +0100 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2024-12-04 03:02:30 +0100 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2024-12-04 03:03:25 +0100 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2024-12-04 03:34:23 +0100 | OftenFaded | (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 2024-12-04 04:06:57 +0100 | td_ | (~td@i5387091F.versanet.de) (Ping timeout: 248 seconds) |
| 2024-12-04 04:08:59 +0100 | td_ | (~td@i53870906.versanet.de) td_ |
| 2024-12-04 04:31:58 +0100 | alp__ | (~alp@128-79-174-146.hfc.dyn.abo.bbox.fr) (Remote host closed the connection) |
| 2024-12-04 04:32:16 +0100 | alp__ | (~alp@2001:861:8ca0:4940:fc7d:2254:175b:29dd) |
| 2024-12-04 04:33:59 +0100 | alp_ | (~alp@2001:861:8ca0:4940:68d:72c1:d8a6:4577) |
| 2024-12-04 04:35:23 +0100 | alp_ | (~alp@2001:861:8ca0:4940:68d:72c1:d8a6:4577) (Remote host closed the connection) |
| 2024-12-04 04:35:40 +0100 | alp_ | (~alp@2001:861:8ca0:4940:1baf:64f4:e1ae:5b74) |
| 2024-12-04 04:37:05 +0100 | alp_ | (~alp@2001:861:8ca0:4940:1baf:64f4:e1ae:5b74) (Remote host closed the connection) |
| 2024-12-04 04:37:09 +0100 | alp__ | (~alp@2001:861:8ca0:4940:fc7d:2254:175b:29dd) (Ping timeout: 252 seconds) |
| 2024-12-04 04:37:22 +0100 | alp_ | (~alp@2001:861:8ca0:4940:4ba7:cb8a:c26a:d8d0) |
| 2024-12-04 04:39:06 +0100 | alp__ | (~alp@2001:861:8ca0:4940:5a62:c4d4:e730:577a) |
| 2024-12-04 04:42:17 +0100 | alp_ | (~alp@2001:861:8ca0:4940:4ba7:cb8a:c26a:d8d0) (Ping timeout: 252 seconds) |
| 2024-12-04 04:44:07 +0100 | alp__ | (~alp@2001:861:8ca0:4940:5a62:c4d4:e730:577a) (Ping timeout: 252 seconds) |
| 2024-12-04 05:31:07 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-12-04 05:47:33 +0100 | T_X | (~T_X@diktynna.open-mesh.org) (Ping timeout: 252 seconds) |
| 2024-12-04 05:59:27 +0100 | T_X | (~T_X@diktynna.open-mesh.org) T_X |
| 2024-12-04 06:04:50 +0100 | T_X | (~T_X@diktynna.open-mesh.org) (Ping timeout: 248 seconds) |
| 2024-12-04 06:15:54 +0100 | T_X | (~T_X@diktynna.open-mesh.org) T_X |
| 2024-12-04 07:57:36 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2024-12-04 07:59:13 +0100 | alp | (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) |
| 2024-12-04 08:02:43 +0100 | alp | (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) (Remote host closed the connection) |
| 2024-12-04 08:03:20 +0100 | alp | (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) |
| 2024-12-04 08:31:50 +0100 | ft | (~ft@p508db9c7.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-12-04 09:56:38 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2024-12-04 12:00:38 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2024-12-04 12:25:20 +0100 | alp | (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) (Ping timeout: 260 seconds) |
| 2024-12-04 13:16:42 +0100 | alp | (~alp@2001:861:8ca0:4940:7c92:cf4a:cc5b:7dc2) |
| 2024-12-04 13:28:40 +0100 | alp | (~alp@2001:861:8ca0:4940:7c92:cf4a:cc5b:7dc2) (Remote host closed the connection) |
| 2024-12-04 13:29:03 +0100 | alp | (~alp@2001:861:8ca0:4940:e895:2263:cae3:811) |
| 2024-12-04 13:56:46 +0100 | portnov | (~portnov@v-20678-unlim.vpn.mgn.ru) portnov |
| 2024-12-04 13:58:52 +0100 | portnov | (~portnov@v-20678-unlim.vpn.mgn.ru) () |
| 2024-12-04 15:08:29 +0100 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2024-12-04 16:30:41 +0100 | alp | (~alp@2001:861:8ca0:4940:e895:2263:cae3:811) (Ping timeout: 252 seconds) |
| 2024-12-04 16:37:11 +0100 | alp | (~alp@2001:861:8ca0:4940:7ce9:459b:14a1:a2de) |
| 2024-12-04 16:56:22 +0100 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2024-12-04 17:35:53 +0100 | alp_ | (~alp@2001:861:8ca0:4940:9c1:764:1276:4604) |
| 2024-12-04 17:38:36 +0100 | alp | (~alp@2001:861:8ca0:4940:7ce9:459b:14a1:a2de) (Ping timeout: 272 seconds) |
| 2024-12-04 17:49:09 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) ash3en |
| 2024-12-04 17:53:01 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Client Quit) |
| 2024-12-04 18:13:42 +0100 | Leary | (~Leary@user/Leary/x-0910699) (Remote host closed the connection) |
| 2024-12-04 19:11:48 +0100 | alp_ | (~alp@2001:861:8ca0:4940:9c1:764:1276:4604) (Remote host closed the connection) |
| 2024-12-04 19:12:36 +0100 | alp | (~alp@2001:861:8ca0:4940:aa17:2267:ede3:dd49) |
| 2024-12-04 19:14:16 +0100 | alp | (~alp@2001:861:8ca0:4940:aa17:2267:ede3:dd49) (Remote host closed the connection) |
| 2024-12-04 19:14:33 +0100 | alp | (~alp@2001:861:8ca0:4940:ce1e:7443:2bff:952b) |
| 2024-12-04 19:21:21 +0100 | alp | (~alp@2001:861:8ca0:4940:ce1e:7443:2bff:952b) (Remote host closed the connection) |
| 2024-12-04 19:21:39 +0100 | alp | (~alp@2001:861:8ca0:4940:8eac:f601:9281:f0e1) |
| 2024-12-04 19:22:33 +0100 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2024-12-04 19:23:03 +0100 | alp | (~alp@2001:861:8ca0:4940:8eac:f601:9281:f0e1) (Remote host closed the connection) |
| 2024-12-04 19:23:20 +0100 | alp | (~alp@2001:861:8ca0:4940:2495:aa5d:f835:c4d7) |
| 2024-12-04 19:24:06 +0100 | <OftenFaded> | what does 'formally proven core' mean in the welcome message context? |
| 2024-12-04 19:24:43 +0100 | alp | (~alp@2001:861:8ca0:4940:2495:aa5d:f835:c4d7) (Remote host closed the connection) |
| 2024-12-04 19:25:00 +0100 | alp | (~alp@2001:861:8ca0:4940:bd22:8dd:6c10:c5e0) |
| 2024-12-04 19:26:25 +0100 | alp | (~alp@2001:861:8ca0:4940:bd22:8dd:6c10:c5e0) (Remote host closed the connection) |
| 2024-12-04 19:26:27 +0100 | <haskellbridge> | <Tranquil Ity> Welcome message ? |
| 2024-12-04 19:26:42 +0100 | alp | (~alp@2001:861:8ca0:4940:1ca2:997d:5ece:75da) |
| 2024-12-04 19:27:33 +0100 | beastwick | (~brian@user/beastwick) (WeeChat 4.4.2) |
| 2024-12-04 19:28:06 +0100 | alp | (~alp@2001:861:8ca0:4940:1ca2:997d:5ece:75da) (Remote host closed the connection) |
| 2024-12-04 19:28:20 +0100 | <OftenFaded> | sorry, I don't know the exact terminology but the short info blurb that has links to cheetsheets and the logs |
| 2024-12-04 19:28:23 +0100 | alp | (~alp@2001:861:8ca0:4940:176d:44a4:3e5:e4a9) |
| 2024-12-04 19:28:33 +0100 | <OftenFaded> | 'xmonad: the tiling window manager with a formally proven core |' |
| 2024-12-04 19:29:47 +0100 | alp | (~alp@2001:861:8ca0:4940:176d:44a4:3e5:e4a9) (Remote host closed the connection) |
| 2024-12-04 19:30:05 +0100 | alp | (~alp@2001:861:8ca0:4940:95ee:27bd:823f:53b4) |
| 2024-12-04 19:31:29 +0100 | alp | (~alp@2001:861:8ca0:4940:95ee:27bd:823f:53b4) (Remote host closed the connection) |
| 2024-12-04 19:31:46 +0100 | alp | (~alp@2001:861:8ca0:4940:5b10:bb7b:d799:e1a) |
| 2024-12-04 19:33:10 +0100 | alp | (~alp@2001:861:8ca0:4940:5b10:bb7b:d799:e1a) (Remote host closed the connection) |
| 2024-12-04 19:33:27 +0100 | alp | (~alp@2001:861:8ca0:4940:bffe:bef:d5fd:3228) |
| 2024-12-04 19:34:28 +0100 | <geekosaur> | the StackSet, which is the core of xmonad that everything else is based on, was translated to the Idris proof assistant (which is very Haskell-like) and formally verified |
| 2024-12-04 19:34:46 +0100 | <geekosaur> | and separately translated to Coq and verified there |
| 2024-12-04 19:35:09 +0100 | alp_ | (~alp@2001:861:8ca0:4940:b9a2:1759:6304:ffae) |
| 2024-12-04 19:35:29 +0100 | <geekosaur> | although that one is less reliable because Coq isn't very Haskell-like so it may depend on the translation a bit |
| 2024-12-04 19:36:53 +0100 | alp__ | (~alp@2001:861:8ca0:4940:563c:b90a:93c1:efa) |
| 2024-12-04 19:37:31 +0100 | <OftenFaded> | so it means like verified to be without bugs or like verified as non-malicious? I'm assuming verification is good in some sense |
| 2024-12-04 19:38:21 +0100 | alp | (~alp@2001:861:8ca0:4940:bffe:bef:d5fd:3228) (Ping timeout: 246 seconds) |
| 2024-12-04 19:39:21 +0100 | <geekosaur> | not quite either. non-maliciousness can't be tested that way, and there's a famous Knuth quote about formal verification |
| 2024-12-04 19:39:33 +0100 | <geekosaur> | "Beware, I have only proven this correct, not tested it" |
| 2024-12-04 19:39:49 +0100 | <geekosaur> | it is _mathematically_ correct |
| 2024-12-04 19:40:06 +0100 | alp_ | (~alp@2001:861:8ca0:4940:b9a2:1759:6304:ffae) (Ping timeout: 246 seconds) |
| 2024-12-04 19:40:39 +0100 | <geekosaur> | this _usually_ means you can consider it bug-free, but there's always the possibility that what it models isn't what you actually want it to do (and in fact it handles floating windows fairly poorly) |
| 2024-12-04 19:41:42 +0100 | L29Ah | rearranges geekosaur's Tabbed while he's busy with his floating window |
| 2024-12-04 19:41:51 +0100 | alp__ | (~alp@2001:861:8ca0:4940:563c:b90a:93c1:efa) (Ping timeout: 246 seconds) |
| 2024-12-04 19:42:23 +0100 | <geekosaur> | (basically, good mathematics doesn't mean good UX) |
| 2024-12-04 19:42:39 +0100 | <OftenFaded> | Very cool. But I'm an idiot, I thought mathematically incorrect code will simply not compile or run (or finish being interpretted) at all no matter what language it is |
| 2024-12-04 19:43:56 +0100 | <OftenFaded> | I don't mean to infinitely bore you with questions if there's some link that will break it down for the unacademic |
| 2024-12-04 19:43:58 +0100 | <geekosaur> | you can write garbage that will run in any language. the question, as I said before, is whether it does what you intend |
| 2024-12-04 19:44:23 +0100 | <OftenFaded> | ohhhh intention is the key element I'm missing then |
| 2024-12-04 19:44:54 +0100 | <geekosaur> | right, it's difficult to describe intent mathematically. or in a computer language, for that matter |
| 2024-12-04 19:45:49 +0100 | <geekosaur> | strong types are an attempt to do that. they're not quite enough, at least in Haskell's form. dependently-typed languages get closer but are much harder to use because no matter what it's going to be difficult to describe intent to a computer |
| 2024-12-04 19:47:31 +0100 | <geekosaur> | tests have the same problem: you have to test the right thing, including all the edge cases |
| 2024-12-04 19:52:44 +0100 | <OftenFaded> | If intent is so difficult, why does haskell concern itself with this mathematical correctness to begin with? Or why is this a non-topic concerning other languages? |
| 2024-12-04 19:53:28 +0100 | <haskellbridge> | <Tranquil Ity> OftenFaded: Where ? |
| 2024-12-04 19:53:36 +0100 | <haskellbridge> | <Tranquil Ity> OftenFaded: Oooh |
| 2024-12-04 19:53:41 +0100 | <haskellbridge> | <Tranquil Ity> Where is that from |
| 2024-12-04 19:54:11 +0100 | <OftenFaded> | Is it essentially an attempt at making a most valid or verified toolset? |
| 2024-12-04 19:54:42 +0100 | <haskellbridge> | <Tranquil Ity> geekosaur: Yea, both are very interesting approaches though. In Idris rather than Idris2 tho ? |
| 2024-12-04 19:55:06 +0100 | <geekosaur> | Idris2 didn't exist in 2007 |
| 2024-12-04 19:55:26 +0100 | <haskellbridge> | <Tranquil Ity> geekosaur: Just generate Haskell from Cow 😔 |
| 2024-12-04 19:55:29 +0100 | <geekosaur> | (the STackSet hasn't been changed siince then) |
| 2024-12-04 19:55:32 +0100 | <haskellbridge> | <Tranquil Ity> * Coq |
| 2024-12-04 19:55:33 +0100 | <haskellbridge> | <Tranquil Ity> Ooh |
| 2024-12-04 19:55:40 +0100 | <haskellbridge> | <Tranquil Ity> Yea that's fair |
| 2024-12-04 19:56:06 +0100 | <geekosaur> | it's so core that any changes would probably force the rest of xmonad+contrib to be rewritten |
| 2024-12-04 19:57:36 +0100 | <haskellbridge> | <Tranquil Ity> OftenFaded: ~Haskell's type system, mathematically speaking, is a mess~ |
| 2024-12-04 19:57:48 +0100 | <haskellbridge> | <Tranquil Ity> geekosaur: Oh huh that's interesting |
| 2024-12-04 20:00:50 +0100 | <OftenFaded> | what do you mean by mess, and if this is true, isn't a verification of stability or mathematical reliability kind of a moot point? |
| 2024-12-04 20:02:31 +0100 | <haskellbridge> | <Tranquil Ity> That's why you rewrite it in another language and generate Haskell from that |
| 2024-12-04 20:02:32 +0100 | <haskellbridge> | <Tranquil Ity> https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html |
| 2024-12-04 20:03:09 +0100 | <geekosaur> | right, and also why the StackSet was translated into Idris and Coq for verification |
| 2024-12-04 20:03:48 +0100 | <geekosaur> | Haskell's type system is not suited to that kind of verification |
| 2024-12-04 20:05:07 +0100 | <geekosaur> | also, mathematically speaking, Haskell has neither sum nor product types; it has sums of products |
| 2024-12-04 20:05:47 +0100 | <OftenFaded> | But if floating windows are problematic even with 'verifiably correct' code due to intent itself being problematic, why don't we try different approaches to solving the 'intent' dilemma? Or is this effectively what other languages are trying to do already? |
| 2024-12-04 20:07:37 +0100 | <geekosaur> | no, in our case it's just that everything else is so tied to the StackSet that fixing it would require rewriting the rest of xmonad |
| 2024-12-04 20:07:55 +0100 | <geekosaur> | so we have hacks like TrackFloating |
| 2024-12-04 20:08:18 +0100 | <geekosaur> | and it's not like they don't work at all; see L29Ah's comment |
| 2024-12-04 20:08:29 +0100 | <haskellbridge> | <Tranquil Ity> geekosaur: Meeeh, it depends on how you consider it |
| 2024-12-04 20:08:30 +0100 | <geekosaur> | tiled windows move around when you work with floats |
| 2024-12-04 20:08:47 +0100 | <haskellbridge> | <Tranquil Ity> If you take the traditional Hask then you have both product and coproduct types |
| 2024-12-04 20:09:18 +0100 | <haskellbridge> | <Tranquil Ity> Categorically speaking ofc |
| 2024-12-04 20:17:43 +0100 | <OftenFaded> | haskell and it's tools are conceptually so interesting to me, but I always feel overly challenged trying to maintain a practicality with it all--it's tough to not fall back to less intimidating familiar toolsets even if less fun |
| 2024-12-04 20:23:34 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) ash3en |
| 2024-12-04 20:36:40 +0100 | <OftenFaded> | this is ultimately a laziness, tho isn't it? xmonad and the ilk are technically more practical in the long run, my ignorance horizon is what hinders the correct perspective |
| 2024-12-04 20:37:54 +0100 | <geekosaur> | it's complex. on the one hand, one could claim laziness; on the other, Haskell forces you to "un-learn" a lot of things other languages teach you |
| 2024-12-04 20:38:09 +0100 | <geekosaur> | which is a lot of hard work because our brains don't want to do that |
| 2024-12-04 20:39:10 +0100 | <geekosaur> | that said, the reward is quite high because learning Haskell makes you a better programmer even in other languages |
| 2024-12-04 20:39:23 +0100 | <geekosaur> | but you need to do a lot of work to get there |
| 2024-12-04 20:41:07 +0100 | <OftenFaded> | how does one deal with the anxiety or paranoia that its only useful for improving one's perspective rather than the tool itself being in key senses the best tool for certain jobs/tasks? |
| 2024-12-04 20:42:25 +0100 | <geekosaur> | for me it was immersion: spending some time using it for everything (which for me was hard as I'm very much a right-tool-for-the-job person) |
| 2024-12-04 20:44:14 +0100 | <geekosaur> | but this isn't specific to Haskell, or even to computer languages: it's how you learn natural languages, for example |
| 2024-12-04 20:45:34 +0100 | <OftenFaded> | that makes a lot of sense. If it can be resourceful for almost everything, it's tough to worry about it's merit/utility-value |
| 2024-12-04 20:48:59 +0100 | <L29Ah> | OftenFaded: i'd say haskell is extraordinarily good for writing fast and correct complex parallel+concurrent software |
| 2024-12-04 20:49:29 +0100 | <L29Ah> | i'm not aware of any other tool that excels at this niche |
| 2024-12-04 20:50:45 +0100 | <L29Ah> | due to completely green-thread-able I/O, STM, and decent typing |
| 2024-12-04 20:52:02 +0100 | <geekosaur> | STM's a big feature for such programs. other languages have STM implementations, but their compilers can't catch you misusing them |
| 2024-12-04 20:52:43 +0100 | <geekosaur> | there are a lot of things that you can't safely do in the middle of a transaction. Haskell's typechecker enforces them; rustc, for one example, can't |
| 2024-12-04 20:53:08 +0100 | <geekosaur> | (because they can't be rolled back if the transaction aborts) |
| 2024-12-04 20:55:22 +0100 | <geekosaur> | also purity helps because a lot of things that wouldn't be rollback-able either become so or aren't possible without doing things that the typechecker blocks |
| 2024-12-04 21:05:30 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Quit: ash3en) |
| 2024-12-04 21:10:38 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) ash3en |
| 2024-12-04 21:12:05 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-12-04 22:05:38 +0100 | OftenFaded | (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 2024-12-04 22:10:17 +0100 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2024-12-04 22:18:47 +0100 | ft | (~ft@p508db9c7.dip0.t-ipconnect.de) ft |
| 2024-12-04 22:22:39 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) ash3en |
| 2024-12-04 22:38:10 +0100 | ash3en | (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Quit: ash3en) |
| 2024-12-04 22:43:17 +0100 | tv | (~tv@user/tv) (Read error: Connection reset by peer) |