Logs: liberachat/#haskell
| 2026-01-08 00:37:47 | × | shr\ke quits (~shrike@user/paxhumana) (Changing host) |
| 2026-01-08 00:37:47 | → | shr\ke joins (~shrike@user/shrke:31298) |
| 2026-01-08 00:40:21 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-08 00:42:14 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 2026-01-08 00:46:42 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 00:49:16 | → | raincomplex joins (~rain@user/raincomplex) |
| 2026-01-08 00:51:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 00:52:16 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2026-01-08 00:55:04 | <EvanR> | in the sense that a program is a proof of some theorem, if I can get a computer to give me the correct program that's great. But that's not what we're doing right now with AI |
| 2026-01-08 00:55:48 | <EvanR> | it's more like mass copywrite infringement search |
| 2026-01-08 00:56:35 | <jreicher> | Even correct programs aren't proofs of theorems. "In retrospect it seems to be doing the right thing." |
| 2026-01-08 00:56:38 | <EvanR> | of code that is hardly a proof of anything |
| 2026-01-08 00:56:39 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 2026-01-08 00:57:22 | <EvanR> | jreicher, correct in the sense that I explicitly specified the theorem |
| 2026-01-08 00:57:36 | <EvanR> | not "write me an MMO in haskell" |
| 2026-01-08 00:58:01 | <newmind> | that would be the dream, yeah: provide a spec, and it spits out a program that fulfills that (and while we're at it, also does proofably terminate and run in limited space).. but current AI agents are doing the exact opposite, little more than running in yolo mode and just executing whatever comes to mind.. what i'm proposing is a middle ground: at |
| 2026-01-08 00:58:02 | <newmind> | least run code that's checked by a compiler and can't do anything completely nuts |
| 2026-01-08 00:58:48 | <jreicher> | Even if AI could do it, I think the bigger problem is motivating humans to write specs in the first place. That's been possible for half a century and still almost nobody doesit. |
| 2026-01-08 00:58:49 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 00:59:15 | <EvanR> | that part is beyond my paygrade xD |
| 2026-01-08 00:59:30 | <newmind> | in the meantime, for _a lot_ of real world software problems, it's a lot more grey: people can specify "what they want" only in very loose terms |
| 2026-01-08 01:00:03 | <EvanR> | people with mathematical or engineering maturity are better at specifying what they want or what they have |
| 2026-01-08 01:00:55 | <EvanR> | hopefully that bleeds onto programming at some point |
| 2026-01-08 01:00:56 | <jreicher> | Never thought about this before, but maybe there's a market for AI /only/ because of informal specification. If the spec was formal non-AI program generation might be possible? |
| 2026-01-08 01:01:26 | <geekosaur> | that was the theory behind UML, I think? |
| 2026-01-08 01:01:30 | <ncf> | take it to #haskell-offtopic please, this is not the place to discuss LLMs |
| 2026-01-08 01:02:08 | <EvanR> | yeah I don't see the connection to haskell specifically |
| 2026-01-08 01:02:58 | <jreicher> | Fair |
| 2026-01-08 01:03:10 | → | omidmash5 joins (~omidmash@user/omidmash) |
| 2026-01-08 01:03:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 01:03:39 | <haskellbridge> | <sm> it means that if you come into a space and talk about the ai thing you're building, you need to be ready for all kinds of response |
| 2026-01-08 01:03:41 | <haskellbridge> | <sm> (I'm not excusing rudeness, but I understand it) |
| 2026-01-08 01:05:09 | × | xff0x quits (~xff0x@2405:6580:b080:900:4b0b:90a:cd82:2bd2) (Ping timeout: 244 seconds) |
| 2026-01-08 01:05:09 | × | omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-08 01:05:09 | omidmash5 | is now known as omidmash |
| 2026-01-08 01:06:27 | <newmind> | the connection would be that haskell (or strongly typed languages in particular) provide guardrails and constraints to LLM generated code that does not exist in other languages, including that generated haskell code is safer (not absolutely safe) to generate and run than in most other languages (especially with the Safe extension enabled). but i |
| 2026-01-08 01:06:28 | <newmind> | take your point, i was just generally looking for feedback, viewpoints and ideas |
| 2026-01-08 01:08:00 | × | prite quits (~pritam@user/pritambaral) (Quit: Konversation terminated!) |
| 2026-01-08 01:08:55 | <int-e> | discover new ways in which well-typed programs go wrong |
| 2026-01-08 01:09:40 | <EvanR> | some of those premises about haskell don't add up ... |
| 2026-01-08 01:10:05 | <int-e> | You'd need {-# LANGUAGE AdditivePromises #-} for that. |
| 2026-01-08 01:10:13 | <EvanR> | executing "untrusted" code is still a horrible idea in haskell |
| 2026-01-08 01:10:21 | <EvanR> | and not sure why that's even required |
| 2026-01-08 01:10:34 | <int-e> | > text "why oh why indeed" |
| 2026-01-08 01:10:35 | <lambdabot> | why oh why indeed |
| 2026-01-08 01:11:16 | <EvanR> | the amount of infrastructure required for lambdabot xD |
| 2026-01-08 01:11:34 | <EvanR> | he's running in the equivalent of that underwater prison in avengers |
| 2026-01-08 01:12:27 | <int-e> | huh |
| 2026-01-08 01:13:42 | <newmind> | obviously, yes. and i'd never advocate for blindly running untrusted code either. but it's a lot easier to reason about a function with a type signature than just executing a bash script blindly. it's not meant as a airtight sandbox that holds up against adverserial attacks, but it is another layer. and it is quite a bit more than what current |
| 2026-01-08 01:13:43 | <newmind> | agents are doing |
| 2026-01-08 01:14:36 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 01:15:52 | <int-e> | EvanR: I'm kind of curious what evoked that picture. |
| 2026-01-08 01:17:55 | <EvanR> | haskell itself isn't making code inherently safe, you have whatever layers of stuff and planning for something like an eval bot |
| 2026-01-08 01:18:36 | <EvanR> | in any language |
| 2026-01-08 01:19:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 01:22:03 | <jreicher> | My understanding of type checking has always been that it's only checking whether the programmer has contradicted themselves. The programmer writes the type assertions, and the programmer writes the code. Type checker checks if that set of assertions is inconsistent according to the type inference rules. |
| 2026-01-08 01:22:22 | <jreicher> | Nothing in that guarantees safety. |
| 2026-01-08 01:22:52 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 2026-01-08 01:23:15 | → | bggd joins (~bgg@user/bggd) |
| 2026-01-08 01:23:20 | <newmind> | exactly, the language itself has nothing to do with the inherent safety, that was never my claim. but what it has is a type system that does let you reason where and how IO actually happens. if you need _safety_ you still need sandboxing, vms and whatever else you would use for any other binary |
| 2026-01-08 01:24:48 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-08 01:24:52 | → | divlamir_ joins (~divlamir@user/divlamir) |
| 2026-01-08 01:25:44 | divlamir_ | is now known as divlamir |
| 2026-01-08 01:30:24 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 01:36:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-08 01:42:00 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 2026-01-08 01:42:13 | × | Googulator14 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-08 01:42:30 | → | Googulator14 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 2026-01-08 01:45:07 | × | lbseale quits (~quassel@user/ep1ctetus) (Client Quit) |
| 2026-01-08 01:45:50 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 2026-01-08 01:48:27 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 01:53:24 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-08 02:00:54 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-08 02:00:56 | → | omidmash1 joins (~omidmash@user/omidmash) |
| 2026-01-08 02:02:30 | × | omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-08 02:02:30 | omidmash1 | is now known as omidmash |
| 2026-01-08 02:04:09 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-08 02:04:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 02:09:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-08 02:09:09 | → | libertyprime joins (~libertypr@121.74.62.77) |
| 2026-01-08 02:09:22 | <monochrom> | You can extend that argument to all correctness proofs. The proof only checks that the program doesn't contradict the claim. Nothing says the claim guarantees safety in the first place. |
| 2026-01-08 02:10:39 | <geekosaur> | (or anything else, for that matter) |
| 2026-01-08 02:10:52 | <monochrom> | But the apologetic is that if you make you say the same thing in two ways, once as the program and once more as the claim, and if they are consistent, that's heightened confidence that you have made fewer mistakes. |
| 2026-01-08 02:11:08 | <monochrom> | err, s/if you make you/if I make you/ |
| 2026-01-08 02:12:47 | <EvanR> | I write my program from scratch several times so there's less chance of a bug |
| 2026-01-08 02:12:51 | <monochrom> | Extra credit if you also provide test cases. (That's like saying the same thing the third way.) |
| 2026-01-08 02:13:20 | <EvanR> | 99% times 99% times 99% correct equals |
| 2026-01-08 02:13:29 | <EvanR> | 999999% correct |
| 2026-01-08 02:14:06 | × | libertyprime quits (~libertypr@121.74.62.77) (Quit: leaving) |
| 2026-01-08 02:14:14 | <monochrom> | (In fact when I pose a programming homework question when teaching, I provide examples and sample test cases. It's good old reliability by redundancy.) |
| 2026-01-08 02:20:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 02:23:08 | × | rainbyte quits (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 2026-01-08 02:24:42 | → | rainbyte joins (~rainbyte@186.22.19.214) |
| 2026-01-08 02:24:52 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-08 02:26:52 | <EvanR> | now I ran into a funny... in some cases repeating a test causes your confidence to go from 95% to 99% to 99.99999%, in other cases repeated trials causes chance of success to go from 95% 30% 2% xD |
| 2026-01-08 02:27:19 | × | rekahsoft quits (~rekahsoft@70.51.99.245) (Ping timeout: 246 seconds) |
| 2026-01-08 02:27:42 | <EvanR> | probability is so subjective |
| 2026-01-08 02:29:39 | <monochrom> | Just rebrand, akak move the goalpost. If the chance of success drops, then speak of the chance of reproducing a heisenbug. >:) |
| 2026-01-08 02:31:08 | <newmind> | or if you have 499 testcases that pass, and one that fails, guess which one is the interesting one? |
| 2026-01-08 02:31:33 | <monochrom> | I guess moving the goalpost to the opposite side entirely is not what people think when they move the goalpost. >:) |
All times are in UTC.