Newest at the top
| 2026-04-27 18:47:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 18:46:30 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Ping timeout: 244 seconds) |
| 2026-04-27 18:45:10 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-04-27 18:44:35 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-27 18:41:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-27 18:36:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 18:32:51 +0000 | <EvanR> | that's just an intermediate form of proving things by cases |
| 2026-04-27 18:29:10 +0000 | doyougnu | (~user@38.175.72.111) (Client Quit) |
| 2026-04-27 18:29:00 +0000 | doyougnu | (~user@38.175.72.111) doyougnu |
| 2026-04-27 18:28:36 +0000 | doyougnu | (~user@38.175.72.111) (Client Quit) |
| 2026-04-27 18:26:22 +0000 | doyougnu | (~user@38.175.72.111) doyougnu |
| 2026-04-27 18:25:35 +0000 | doyougnu | (~user@38.175.72.111) (Remote host closed the connection) |
| 2026-04-27 18:25:25 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-27 18:23:06 +0000 | doyougnu | (~user@38.175.72.111) doyougnu |
| 2026-04-27 18:20:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 18:19:50 +0000 | doyougnu- | (~doyougnu@38.175.72.111) doyougnu- |
| 2026-04-27 18:18:33 +0000 | doyougnu | (~doyougnu@38.175.72.111) (Killed (NickServ (GHOST command used by doyougnu`!~user@38.175.72.111))) |
| 2026-04-27 18:17:07 +0000 | <davean> | "Whats the smallest valid test type?" "Ok, now why isn't that a proof already?" |
| 2026-04-27 18:14:32 +0000 | <davean> | You have to start by articulating why the version is the same but smaller ... and now you've listed the cases ... |
| 2026-04-27 18:14:06 +0000 | <davean> | though the "making a small enough version" ... gets you very close to a proof ... |
| 2026-04-27 18:13:39 +0000 | <davean> | And often via paramatricity one can make a small enough version too |
| 2026-04-27 18:12:51 +0000 | <monochrom> | Yeah. |
| 2026-04-27 18:12:39 +0000 | <davean> | Lots of things *are* small enough |
| 2026-04-27 18:12:29 +0000 | <davean> | monochrom: I do think more things should be tested by enumeration. Its not an unreasonable strat. |
| 2026-04-27 18:10:38 +0000 | Alex_delenda_est | (~al_test@178.34.162.165) |
| 2026-04-27 18:09:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 18:06:53 +0000 | <EvanR> | Deimos Anomaly |
| 2026-04-27 18:06:28 +0000 | <EvanR> | FP4 (E2M1) |
| 2026-04-27 18:05:35 +0000 | ft | (~ft@p508db287.dip0.t-ipconnect.de) ft |
| 2026-04-27 18:05:32 +0000 | <davean> | https://en.wikipedia.org/wiki/Block_floating_point |
| 2026-04-27 18:04:47 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-27 18:04:28 +0000 | <EvanR> | not necessarily a good reason (AI) xD |
| 2026-04-27 18:04:11 +0000 | <davean> | and there is a reason its got that "NV" tacked on the front |
| 2026-04-27 18:04:00 +0000 | <davean> | There is a reason there is an NVFP4 |
| 2026-04-27 18:03:49 +0000 | <EvanR> | I'm sure eighth precision has some application somehow |
| 2026-04-27 18:02:58 +0000 | <davean> | EvanR: you're joking but I'm refering to actual datatypes |
| 2026-04-27 18:02:40 +0000 | <EvanR> | half is 16 so... quarter... eighth precision |
| 2026-04-27 18:02:38 +0000 | <davean> | NVFP4 if you're in AI |
| 2026-04-27 18:02:19 +0000 | <davean> | FP4 |
| 2026-04-27 18:02:18 +0000 | <monochrom> | toy example I would use in class to teach floating point :) |
| 2026-04-27 18:02:16 +0000 | <davean> | I did feed it both anyway, this is weird because I remember taking time to type that out ... but maybe I lost it in a quick reply to monochrom |
| 2026-04-27 18:01:59 +0000 | <EvanR> | what would you call a float with 4 total bits |
| 2026-04-27 18:01:47 +0000 | <davean> | EvanR: yes, 4 bits |
| 2026-04-27 18:01:36 +0000 | <davean> | I sure meant to type Int4/Word4 |
| 2026-04-27 18:01:35 +0000 | <monochrom> | Hey I haven't used Int4 for a while! Last time it was Casio FX-702P which was fabled to combine two 4-bit CPUs to do 8-bit work. |
| 2026-04-27 18:01:25 +0000 | <davean> | er didn't I? |
| 2026-04-27 18:01:21 +0000 | <EvanR> | four bits? |
| 2026-04-27 18:01:17 +0000 | <davean> | ijouw: I said I used both |
| 2026-04-27 18:01:03 +0000 | <haskellbridge> | <ijouw> Int4 or Word4? |
| 2026-04-27 18:00:42 +0000 | <davean> | I just consider int4 trivially small! |