Logs: liberachat/#haskell
| 2026-04-27 16:20:23 | × | jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2026-04-27 16:23:16 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-27 16:23:21 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-04-27 16:29:47 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 265 seconds) |
| 2026-04-27 16:29:57 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 16:34:57 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 16:38:38 | × | hellwolf quits (~user@13ba-9fa1-c9b7-72ee-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 252 seconds) |
| 2026-04-27 16:39:37 | ← | thenightmail` parts (~whoareyou@user/thenightmail) (ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.2)) |
| 2026-04-27 16:41:43 | → | hellwolf joins (~user@85eb-3c61-7214-710f-0f00-4d40-07d0-2001.sta.estpak.ee) |
| 2026-04-27 16:45:44 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 16:50:21 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-04-27 16:50:39 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-04-27 16:57:03 | → | thenightmail` joins (~whoareyou@user/thenightmail) |
| 2026-04-27 16:57:14 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2026-04-27 17:01:31 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 17:06:27 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 17:06:33 | → | Enrico63 joins (~Enrico63@85.255.235.90) |
| 2026-04-27 17:08:29 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-27 17:13:00 | → | layline_ joins (~layline@149.154.26.56) |
| 2026-04-27 17:16:29 | × | tromp quits (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-27 17:17:08 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 17:17:38 | × | jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 248 seconds) |
| 2026-04-27 17:18:19 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-27 17:21:12 | <davean> | Yah, the way you usually prove the tests are exhaustive is equivilent to just proving it directly if the state space isn't trivially small :) |
| 2026-04-27 17:21:50 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 17:32:57 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 17:33:31 | → | tromp joins (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) |
| 2026-04-27 17:37:57 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 17:42:06 | × | Enrico63 quits (~Enrico63@85.255.235.90) (Quit: Client closed) |
| 2026-04-27 17:46:44 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 17:53:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-27 17:56:31 | <monochrom> | If you have "data X = C1 | C2 | C3; f :: X -> Int" then exhaustive testing is proof, there are only 3 cases to check. |
| 2026-04-27 17:57:40 | <davean> | Note the "trivially small" caviate :) |
| 2026-04-27 17:58:06 | <monochrom> | I missed that. Sorry! |
| 2026-04-27 17:58:09 | <EvanR> | an ultrafinitist might take exception calling X trivially small! |
| 2026-04-27 17:58:29 | <EvanR> | 4 might be the largest possible number |
| 2026-04-27 17:58:44 | <davean> | EvanR: Get me an ultrafinitist with a broader view then :) |
| 2026-04-27 17:58:59 | <davean> | I want more inclusive ultrafinitists |
| 2026-04-27 17:59:32 | <monochrom> | I'm a cosmological finitist. I think that 10^80 ought to be enough for everyone. :) |
| 2026-04-27 17:59:55 | <davean> | Yah, how many relations are there between particles in the universe? |
| 2026-04-27 18:00:12 | <haskellbridge> | <ijouw> Now I am trying to imagine an exclusive untrainfinitist |
| 2026-04-27 18:00:29 | <davean> | I did test a searcg implimentation once by making it pametric and feeding it Int4 and testing all cases ... |
| 2026-04-27 18:00:34 | <davean> | I'm not against that. |
| 2026-04-27 18:00:40 | <EvanR> | 10^80 cripples combinatorialists |
| 2026-04-27 18:00:42 | <davean> | I just consider int4 trivially small! |
| 2026-04-27 18:01:03 | <haskellbridge> | <ijouw> Int4 or Word4? |
| 2026-04-27 18:01:17 | <davean> | ijouw: I said I used both |
| 2026-04-27 18:01:21 | <EvanR> | four bits? |
| 2026-04-27 18:01:25 | <davean> | er didn't I? |
| 2026-04-27 18:01:35 | <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:36 | <davean> | I sure meant to type Int4/Word4 |
| 2026-04-27 18:01:47 | <davean> | EvanR: yes, 4 bits |
| 2026-04-27 18:01:59 | <EvanR> | what would you call a float with 4 total bits |
| 2026-04-27 18:02:16 | <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:02:18 | <monochrom> | toy example I would use in class to teach floating point :) |
| 2026-04-27 18:02:19 | <davean> | FP4 |
| 2026-04-27 18:02:38 | <davean> | NVFP4 if you're in AI |
| 2026-04-27 18:02:40 | <EvanR> | half is 16 so... quarter... eighth precision |
| 2026-04-27 18:02:58 | <davean> | EvanR: you're joking but I'm refering to actual datatypes |
| 2026-04-27 18:03:49 | <EvanR> | I'm sure eighth precision has some application somehow |
| 2026-04-27 18:04:00 | <davean> | There is a reason there is an NVFP4 |
| 2026-04-27 18:04:11 | <davean> | and there is a reason its got that "NV" tacked on the front |
| 2026-04-27 18:04:28 | <EvanR> | not necessarily a good reason (AI) xD |
| 2026-04-27 18:04:47 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 18:05:32 | <davean> | https://en.wikipedia.org/wiki/Block_floating_point |
| 2026-04-27 18:05:35 | → | ft joins (~ft@p508db287.dip0.t-ipconnect.de) |
| 2026-04-27 18:06:28 | <EvanR> | FP4 (E2M1) |
| 2026-04-27 18:06:53 | <EvanR> | Deimos Anomaly |
| 2026-04-27 18:09:54 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 18:10:38 | → | Alex_delenda_est joins (~al_test@178.34.162.165) |
| 2026-04-27 18:12:29 | <davean> | monochrom: I do think more things should be tested by enumeration. Its not an unreasonable strat. |
| 2026-04-27 18:12:39 | <davean> | Lots of things *are* small enough |
| 2026-04-27 18:12:51 | <monochrom> | Yeah. |
| 2026-04-27 18:13:39 | <davean> | And often via paramatricity one can make a small enough version too |
| 2026-04-27 18:14:06 | <davean> | though the "making a small enough version" ... gets you very close to a proof ... |
| 2026-04-27 18:14:32 | <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:17:07 | <davean> | "Whats the smallest valid test type?" "Ok, now why isn't that a proof already?" |
| 2026-04-27 18:18:33 | × | doyougnu quits (~doyougnu@38.175.72.111) (Killed (NickServ (GHOST command used by doyougnu`!~user@38.175.72.111))) |
| 2026-04-27 18:19:50 | → | doyougnu- joins (~doyougnu@38.175.72.111) |
| 2026-04-27 18:20:34 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 18:23:06 | → | doyougnu joins (~user@38.175.72.111) |
| 2026-04-27 18:25:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-27 18:25:35 | × | doyougnu quits (~user@38.175.72.111) (Remote host closed the connection) |
| 2026-04-27 18:26:22 | → | doyougnu joins (~user@38.175.72.111) |
| 2026-04-27 18:28:36 | × | doyougnu quits (~user@38.175.72.111) (Client Quit) |
| 2026-04-27 18:29:00 | → | doyougnu joins (~user@38.175.72.111) |
| 2026-04-27 18:29:10 | × | doyougnu quits (~user@38.175.72.111) (Client Quit) |
| 2026-04-27 18:32:51 | <EvanR> | that's just an intermediate form of proving things by cases |
| 2026-04-27 18:36:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 18:41:17 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-27 18:44:35 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-27 18:45:10 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-04-27 18:46:30 | × | dtman34 quits (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Ping timeout: 244 seconds) |
| 2026-04-27 18:47:46 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 18:48:40 | layline_ | is now known as layline-away |
| 2026-04-27 18:49:23 | jmcantrell_ | is now known as jmcantrell |
| 2026-04-27 18:50:03 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2026-04-27 18:52:12 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 18:57:07 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-04-27 19:00:11 | × | redshuffle quits (~quassel@45.43.70.75) (Remote host closed the connection) |
All times are in UTC.