Logs on 2024-12-04 (liberachat/#xmonad)
| 00:00:08 | × | alp_ quits (~alp@2001:861:8ca0:4940:5aee:7e5d:1206:a620) (Remote host closed the connection) |
| 00:00:25 | → | alp_ joins (~alp@2001:861:8ca0:4940:a886:2477:d10a:75c1) |
| 00:02:09 | → | alp__ joins (~alp@128-79-174-146.hfc.dyn.abo.bbox.fr) |
| 00:05:13 | × | alp_ quits (~alp@2001:861:8ca0:4940:a886:2477:d10a:75c1) (Ping timeout: 252 seconds) |
| 00:34:51 | × | OftenFaded quits (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 01:04:36 | → | OftenFaded joins (~OftenFade@user/tisktisk) |
| 02:02:30 | × | Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 02:03:25 | → | Buliarous joins (~gypsydang@46.232.210.139) |
| 02:34:23 | × | OftenFaded quits (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 03:06:57 | × | td_ quits (~td@i5387091F.versanet.de) (Ping timeout: 248 seconds) |
| 03:08:59 | → | td_ joins (~td@i53870906.versanet.de) |
| 03:31:58 | × | alp__ quits (~alp@128-79-174-146.hfc.dyn.abo.bbox.fr) (Remote host closed the connection) |
| 03:32:16 | → | alp__ joins (~alp@2001:861:8ca0:4940:fc7d:2254:175b:29dd) |
| 03:33:59 | → | alp_ joins (~alp@2001:861:8ca0:4940:68d:72c1:d8a6:4577) |
| 03:35:23 | × | alp_ quits (~alp@2001:861:8ca0:4940:68d:72c1:d8a6:4577) (Remote host closed the connection) |
| 03:35:40 | → | alp_ joins (~alp@2001:861:8ca0:4940:1baf:64f4:e1ae:5b74) |
| 03:37:05 | × | alp_ quits (~alp@2001:861:8ca0:4940:1baf:64f4:e1ae:5b74) (Remote host closed the connection) |
| 03:37:09 | × | alp__ quits (~alp@2001:861:8ca0:4940:fc7d:2254:175b:29dd) (Ping timeout: 252 seconds) |
| 03:37:22 | → | alp_ joins (~alp@2001:861:8ca0:4940:4ba7:cb8a:c26a:d8d0) |
| 03:39:06 | → | alp__ joins (~alp@2001:861:8ca0:4940:5a62:c4d4:e730:577a) |
| 03:42:17 | × | alp_ quits (~alp@2001:861:8ca0:4940:4ba7:cb8a:c26a:d8d0) (Ping timeout: 252 seconds) |
| 03:44:07 | × | alp__ quits (~alp@2001:861:8ca0:4940:5a62:c4d4:e730:577a) (Ping timeout: 252 seconds) |
| 04:31:07 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 04:47:33 | × | T_X quits (~T_X@diktynna.open-mesh.org) (Ping timeout: 252 seconds) |
| 04:59:27 | → | T_X joins (~T_X@diktynna.open-mesh.org) |
| 05:04:50 | × | T_X quits (~T_X@diktynna.open-mesh.org) (Ping timeout: 248 seconds) |
| 05:15:54 | → | T_X joins (~T_X@diktynna.open-mesh.org) |
| 06:57:36 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 06:59:13 | → | alp joins (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) |
| 07:02:43 | × | alp quits (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) (Remote host closed the connection) |
| 07:03:20 | → | alp joins (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) |
| 07:31:50 | × | ft quits (~ft@p508db9c7.dip0.t-ipconnect.de) (Quit: leaving) |
| 08:56:38 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 11:00:38 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:25:20 | × | alp quits (~alp@2001:861:8ca0:4940:81a9:6af:7f50:e369) (Ping timeout: 260 seconds) |
| 12:16:42 | → | alp joins (~alp@2001:861:8ca0:4940:7c92:cf4a:cc5b:7dc2) |
| 12:28:40 | × | alp quits (~alp@2001:861:8ca0:4940:7c92:cf4a:cc5b:7dc2) (Remote host closed the connection) |
| 12:29:03 | → | alp joins (~alp@2001:861:8ca0:4940:e895:2263:cae3:811) |
| 12:56:46 | → | portnov joins (~portnov@v-20678-unlim.vpn.mgn.ru) |
| 12:58:52 | ← | portnov parts (~portnov@v-20678-unlim.vpn.mgn.ru) () |
| 14:08:29 | → | hiecaq joins (~hiecaq@user/hiecaq) |
| 15:30:41 | × | alp quits (~alp@2001:861:8ca0:4940:e895:2263:cae3:811) (Ping timeout: 252 seconds) |
| 15:37:11 | → | alp joins (~alp@2001:861:8ca0:4940:7ce9:459b:14a1:a2de) |
| 15:56:22 | × | hiecaq quits (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 16:35:53 | → | alp_ joins (~alp@2001:861:8ca0:4940:9c1:764:1276:4604) |
| 16:38:36 | × | alp quits (~alp@2001:861:8ca0:4940:7ce9:459b:14a1:a2de) (Ping timeout: 272 seconds) |
| 16:49:09 | → | ash3en joins (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) |
| 16:53:01 | × | ash3en quits (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Client Quit) |
| 17:13:42 | × | Leary quits (~Leary@user/Leary/x-0910699) (Remote host closed the connection) |
| 18:11:48 | × | alp_ quits (~alp@2001:861:8ca0:4940:9c1:764:1276:4604) (Remote host closed the connection) |
| 18:12:36 | → | alp joins (~alp@2001:861:8ca0:4940:aa17:2267:ede3:dd49) |
| 18:14:16 | × | alp quits (~alp@2001:861:8ca0:4940:aa17:2267:ede3:dd49) (Remote host closed the connection) |
| 18:14:33 | → | alp joins (~alp@2001:861:8ca0:4940:ce1e:7443:2bff:952b) |
| 18:21:21 | × | alp quits (~alp@2001:861:8ca0:4940:ce1e:7443:2bff:952b) (Remote host closed the connection) |
| 18:21:39 | → | alp joins (~alp@2001:861:8ca0:4940:8eac:f601:9281:f0e1) |
| 18:22:33 | → | OftenFaded joins (~OftenFade@user/tisktisk) |
| 18:23:03 | × | alp quits (~alp@2001:861:8ca0:4940:8eac:f601:9281:f0e1) (Remote host closed the connection) |
| 18:23:20 | → | alp joins (~alp@2001:861:8ca0:4940:2495:aa5d:f835:c4d7) |
| 18:24:06 | <OftenFaded> | what does 'formally proven core' mean in the welcome message context? |
| 18:24:43 | × | alp quits (~alp@2001:861:8ca0:4940:2495:aa5d:f835:c4d7) (Remote host closed the connection) |
| 18:25:00 | → | alp joins (~alp@2001:861:8ca0:4940:bd22:8dd:6c10:c5e0) |
| 18:26:25 | × | alp quits (~alp@2001:861:8ca0:4940:bd22:8dd:6c10:c5e0) (Remote host closed the connection) |
| 18:26:27 | <haskellbridge> | <Tranquil Ity> Welcome message ? |
| 18:26:42 | → | alp joins (~alp@2001:861:8ca0:4940:1ca2:997d:5ece:75da) |
| 18:27:33 | ← | beastwick parts (~brian@user/beastwick) (WeeChat 4.4.2) |
| 18:28:06 | × | alp quits (~alp@2001:861:8ca0:4940:1ca2:997d:5ece:75da) (Remote host closed the connection) |
| 18:28:20 | <OftenFaded> | sorry, I don't know the exact terminology but the short info blurb that has links to cheetsheets and the logs |
| 18:28:23 | → | alp joins (~alp@2001:861:8ca0:4940:176d:44a4:3e5:e4a9) |
| 18:28:33 | <OftenFaded> | 'xmonad: the tiling window manager with a formally proven core |' |
| 18:29:47 | × | alp quits (~alp@2001:861:8ca0:4940:176d:44a4:3e5:e4a9) (Remote host closed the connection) |
| 18:30:05 | → | alp joins (~alp@2001:861:8ca0:4940:95ee:27bd:823f:53b4) |
| 18:31:29 | × | alp quits (~alp@2001:861:8ca0:4940:95ee:27bd:823f:53b4) (Remote host closed the connection) |
| 18:31:46 | → | alp joins (~alp@2001:861:8ca0:4940:5b10:bb7b:d799:e1a) |
| 18:33:10 | × | alp quits (~alp@2001:861:8ca0:4940:5b10:bb7b:d799:e1a) (Remote host closed the connection) |
| 18:33:27 | → | alp joins (~alp@2001:861:8ca0:4940:bffe:bef:d5fd:3228) |
| 18:34:28 | <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 |
| 18:34:46 | <geekosaur> | and separately translated to Coq and verified there |
| 18:35:09 | → | alp_ joins (~alp@2001:861:8ca0:4940:b9a2:1759:6304:ffae) |
| 18:35:29 | <geekosaur> | although that one is less reliable because Coq isn't very Haskell-like so it may depend on the translation a bit |
| 18:36:53 | → | alp__ joins (~alp@2001:861:8ca0:4940:563c:b90a:93c1:efa) |
| 18:37:31 | <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 |
| 18:38:21 | × | alp quits (~alp@2001:861:8ca0:4940:bffe:bef:d5fd:3228) (Ping timeout: 246 seconds) |
| 18:39:21 | <geekosaur> | not quite either. non-maliciousness can't be tested that way, and there's a famous Knuth quote about formal verification |
| 18:39:33 | <geekosaur> | "Beware, I have only proven this correct, not tested it" |
| 18:39:49 | <geekosaur> | it is _mathematically_ correct |
| 18:40:06 | × | alp_ quits (~alp@2001:861:8ca0:4940:b9a2:1759:6304:ffae) (Ping timeout: 246 seconds) |
| 18:40:39 | <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) |
| 18:41:42 | L29Ah | rearranges geekosaur's Tabbed while he's busy with his floating window |
| 18:41:51 | × | alp__ quits (~alp@2001:861:8ca0:4940:563c:b90a:93c1:efa) (Ping timeout: 246 seconds) |
| 18:42:23 | <geekosaur> | (basically, good mathematics doesn't mean good UX) |
| 18:42:39 | <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 |
| 18:43:56 | <OftenFaded> | I don't mean to infinitely bore you with questions if there's some link that will break it down for the unacademic |
| 18:43:58 | <geekosaur> | you can write garbage that will run in any language. the question, as I said before, is whether it does what you intend |
| 18:44:23 | <OftenFaded> | ohhhh intention is the key element I'm missing then |
| 18:44:54 | <geekosaur> | right, it's difficult to describe intent mathematically. or in a computer language, for that matter |
| 18:45:49 | <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 |
| 18:47:31 | <geekosaur> | tests have the same problem: you have to test the right thing, including all the edge cases |
| 18:52:44 | <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? |
| 18:53:28 | <haskellbridge> | <Tranquil Ity> OftenFaded: Where ? |
| 18:53:36 | <haskellbridge> | <Tranquil Ity> OftenFaded: Oooh |
| 18:53:41 | <haskellbridge> | <Tranquil Ity> Where is that from |
| 18:54:11 | <OftenFaded> | Is it essentially an attempt at making a most valid or verified toolset? |
| 18:54:42 | <haskellbridge> | <Tranquil Ity> geekosaur: Yea, both are very interesting approaches though. In Idris rather than Idris2 tho ? |
| 18:55:06 | <geekosaur> | Idris2 didn't exist in 2007 |
| 18:55:26 | <haskellbridge> | <Tranquil Ity> geekosaur: Just generate Haskell from Cow 😔 |
| 18:55:29 | <geekosaur> | (the STackSet hasn't been changed siince then) |
| 18:55:32 | <haskellbridge> | <Tranquil Ity> * Coq |
| 18:55:33 | <haskellbridge> | <Tranquil Ity> Ooh |
| 18:55:40 | <haskellbridge> | <Tranquil Ity> Yea that's fair |
| 18:56:06 | <geekosaur> | it's so core that any changes would probably force the rest of xmonad+contrib to be rewritten |
| 18:57:36 | <haskellbridge> | <Tranquil Ity> OftenFaded: ~Haskell's type system, mathematically speaking, is a mess~ |
| 18:57:48 | <haskellbridge> | <Tranquil Ity> geekosaur: Oh huh that's interesting |
| 19:00:50 | <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? |
| 19:02:31 | <haskellbridge> | <Tranquil Ity> That's why you rewrite it in another language and generate Haskell from that |
| 19:02:32 | <haskellbridge> | <Tranquil Ity> https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html |
| 19:03:09 | <geekosaur> | right, and also why the StackSet was translated into Idris and Coq for verification |
| 19:03:48 | <geekosaur> | Haskell's type system is not suited to that kind of verification |
| 19:05:07 | <geekosaur> | also, mathematically speaking, Haskell has neither sum nor product types; it has sums of products |
| 19:05:47 | <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? |
| 19:07:37 | <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 |
| 19:07:55 | <geekosaur> | so we have hacks like TrackFloating |
| 19:08:18 | <geekosaur> | and it's not like they don't work at all; see L29Ah's comment |
| 19:08:29 | <haskellbridge> | <Tranquil Ity> geekosaur: Meeeh, it depends on how you consider it |
| 19:08:30 | <geekosaur> | tiled windows move around when you work with floats |
| 19:08:47 | <haskellbridge> | <Tranquil Ity> If you take the traditional Hask then you have both product and coproduct types |
| 19:09:18 | <haskellbridge> | <Tranquil Ity> Categorically speaking ofc |
| 19:17:43 | <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 |
| 19:23:34 | → | ash3en joins (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) |
| 19:36:40 | <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 |
| 19:37:54 | <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 |
| 19:38:09 | <geekosaur> | which is a lot of hard work because our brains don't want to do that |
| 19:39:10 | <geekosaur> | that said, the reward is quite high because learning Haskell makes you a better programmer even in other languages |
| 19:39:23 | <geekosaur> | but you need to do a lot of work to get there |
| 19:41:07 | <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? |
| 19:42:25 | <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) |
| 19:44:14 | <geekosaur> | but this isn't specific to Haskell, or even to computer languages: it's how you learn natural languages, for example |
| 19:45:34 | <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 |
| 19:48:59 | <L29Ah> | OftenFaded: i'd say haskell is extraordinarily good for writing fast and correct complex parallel+concurrent software |
| 19:49:29 | <L29Ah> | i'm not aware of any other tool that excels at this niche |
| 19:50:45 | <L29Ah> | due to completely green-thread-able I/O, STM, and decent typing |
| 19:52:02 | <geekosaur> | STM's a big feature for such programs. other languages have STM implementations, but their compilers can't catch you misusing them |
| 19:52:43 | <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 |
| 19:53:08 | <geekosaur> | (because they can't be rolled back if the transaction aborts) |
| 19:55:22 | <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 |
| 20:05:30 | × | ash3en quits (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Quit: ash3en) |
| 20:10:38 | → | ash3en joins (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) |
| 20:12:05 | × | ash3en quits (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 21:05:38 | × | OftenFaded quits (~OftenFade@user/tisktisk) (Quit: Client closed) |
| 21:10:17 | → | OftenFaded joins (~OftenFade@user/tisktisk) |
| 21:18:47 | → | ft joins (~ft@p508db9c7.dip0.t-ipconnect.de) |
| 21:22:39 | → | ash3en joins (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) |
| 21:38:10 | × | ash3en quits (~Thunderbi@ip1f10cbd6.dynamic.kabel-deutschland.de) (Quit: ash3en) |
| 21:43:17 | × | tv quits (~tv@user/tv) (Read error: Connection reset by peer) |
| 23:52:49 | → | Leary joins (~Leary@user/Leary/x-0910699) |
All times are in UTC on 2024-12-04.