Newest at the top
| 2026-01-08 03:11:08 +0100 | <monochrom> | err, s/if you make you/if I make you/ |
| 2026-01-08 03:10:52 +0100 | <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 03:10:39 +0100 | <geekosaur> | (or anything else, for that matter) |
| 2026-01-08 03:09:22 +0100 | <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 03:09:09 +0100 | libertyprime | (~libertypr@121.74.62.77) libertyprime |
| 2026-01-08 03:09:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-08 03:04:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-08 03:04:09 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-08 03:02:30 +0100 | omidmash1 | omidmash |
| 2026-01-08 03:02:30 +0100 | omidmash | (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-08 03:00:56 +0100 | omidmash1 | (~omidmash@user/omidmash) omidmash |
| 2026-01-08 03:00:54 +0100 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-08 02:53:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-08 02:48:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-08 02:45:50 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2026-01-08 02:45:07 +0100 | lbseale | (~quassel@user/ep1ctetus) (Client Quit) |
| 2026-01-08 02:42:30 +0100 | Googulator14 | (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 2026-01-08 02:42:13 +0100 | Googulator14 | (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-08 02:42:00 +0100 | lbseale | (~quassel@user/ep1ctetus) ep1ctetus |
| 2026-01-08 02:36:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-08 02:30:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-08 02:25:44 +0100 | divlamir_ | divlamir |
| 2026-01-08 02:24:52 +0100 | divlamir_ | (~divlamir@user/divlamir) divlamir |
| 2026-01-08 02:24:48 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-08 02:23:20 +0100 | <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 02:23:15 +0100 | bggd | (~bgg@user/bggd) bggd |
| 2026-01-08 02:22:52 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-08 02:22:22 +0100 | <jreicher> | Nothing in that guarantees safety. |
| 2026-01-08 02:22:03 +0100 | <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 02:19:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 02:18:36 +0100 | <EvanR> | in any language |
| 2026-01-08 02:17:55 +0100 | <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 02:15:52 +0100 | <int-e> | EvanR: I'm kind of curious what evoked that picture. |
| 2026-01-08 02:14:36 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-08 02:13:43 +0100 | <newmind> | agents are doing |
| 2026-01-08 02:13:42 +0100 | <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 02:12:27 +0100 | <int-e> | huh |
| 2026-01-08 02:11:34 +0100 | <EvanR> | he's running in the equivalent of that underwater prison in avengers |
| 2026-01-08 02:11:16 +0100 | <EvanR> | the amount of infrastructure required for lambdabot xD |
| 2026-01-08 02:10:35 +0100 | <lambdabot> | why oh why indeed |
| 2026-01-08 02:10:34 +0100 | <int-e> | > text "why oh why indeed" |
| 2026-01-08 02:10:21 +0100 | <EvanR> | and not sure why that's even required |
| 2026-01-08 02:10:13 +0100 | <EvanR> | executing "untrusted" code is still a horrible idea in haskell |
| 2026-01-08 02:10:05 +0100 | <int-e> | You'd need {-# LANGUAGE AdditivePromises #-} for that. |
| 2026-01-08 02:09:40 +0100 | <EvanR> | some of those premises about haskell don't add up ... |
| 2026-01-08 02:08:55 +0100 | <int-e> | discover new ways in which well-typed programs go wrong |
| 2026-01-08 02:08:00 +0100 | prite | (~pritam@user/pritambaral) (Quit: Konversation terminated!) |
| 2026-01-08 02:06:28 +0100 | <newmind> | take your point, i was just generally looking for feedback, viewpoints and ideas |
| 2026-01-08 02:06:27 +0100 | <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 02:05:09 +0100 | omidmash5 | omidmash |