Newest at the top
| 2026-04-25 13:05:13 +0000 | <jreicher> | In my opinion there's no such thing as a dynamically typed language in this sense. The "program verification" aspect of types disappear as soon as you don't have static type checking. What is meant by "dynamic types" is more like "dynamic dispatch", which is something different |
| 2026-04-25 13:05:02 +0000 | <ski> | raincomplex : looking into property-based testing (like e.g. QuickCheck and similar), and also (preferably higher-order) contract checking (Racket has one), would probably be helpful, as well |
| 2026-04-25 13:04:13 +0000 | <raincomplex> | i'm thinking about the development pattern of making some changes, and then fixing the errors that arise when compiling/running. in a statically typed language, the type system covers more of this than in a dynamically typed language, where you need tests (manual or automated) to trigger the errors |
| 2026-04-25 13:01:25 +0000 | <jreicher> | raincomplex: My hunch is that the infinite/finite distinction is what you're after. If you want to show that a specific set of inputs result in the right behaviour, testing will give you that. But if you're in the realm of "all possible inputs", and that all is either infinite or unfeasibly large, testing won't, but type checking might. |
| 2026-04-25 13:01:21 +0000 | <[exa]> | raincomplex: article more like in "blog post" or "academic paper" |
| 2026-04-25 12:59:57 +0000 | <ski> | (or the caller of it, passing invald inputs) |
| 2026-04-25 12:59:44 +0000 | <ski> | higher-order contract checking systems can also correctly assign blame, when you're passing a callback to some library procedure, determining whether the callback was in breach, or the library operation itself |
| 2026-04-25 12:59:00 +0000 | <ski> | (then there's property testing, that's using randomly generated test cases, according to some coded distribution of inputs, which is quite useful, because it allows you to state testing *properties*, being more general than particular individual test cases) |
| 2026-04-25 12:58:02 +0000 | <jreicher> | Tests won't get you infinite coverage |
| 2026-04-25 12:57:54 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 248 seconds) |
| 2026-04-25 12:57:45 +0000 | <jreicher> | Emphasis on "every". That's what is special about a proof. That "every" is (probably) infinite. |
| 2026-04-25 12:57:42 +0000 | <ski> | tests, and contracts checking more generally, can assign blame for individual run-time issues, but generally can't prove the absence |
| 2026-04-25 12:55:56 +0000 | <ski> | a type system can ensure static properties about every possible future run of an operation |
| 2026-04-25 12:54:58 +0000 | puke | (~puke@user/puke) (Ping timeout: 250 seconds) |
| 2026-04-25 12:54:57 +0000 | <raincomplex> | i'm just looking for a discussion of the differences and overlaps |
| 2026-04-25 12:53:31 +0000 | <jreicher> | raincomplex: what kind of relationship are you expecting? A type check is a proof, but testing.... isn't |
| 2026-04-25 12:53:21 +0000 | <ski> | each can do things that the other can't |
| 2026-04-25 12:53:15 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-04-25 12:50:00 +0000 | nattkyrro | (~serenity@user/nattkyrro) nattkyrro |
| 2026-04-25 12:49:10 +0000 | <raincomplex> | does anybody have a good article about the relationship (or lack thereof) between type systems and tests |
| 2026-04-25 12:42:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-25 12:37:18 +0000 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 256 seconds) |
| 2026-04-25 12:37:16 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 12:30:10 +0000 | tremon | (~tremon@83.80.159.219) tremon |
| 2026-04-25 12:26:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-04-25 12:25:22 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-25 12:24:52 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-25 12:21:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 12:17:28 +0000 | puke | (~puke@user/puke) puke |
| 2026-04-25 12:16:49 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-25 12:11:40 +0000 | xff0x | (~xff0x@ah206235.dynamic.ppp.asahi-net.or.jp) |
| 2026-04-25 12:10:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-25 12:08:18 +0000 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2026-04-25 12:05:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 11:57:06 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-25 11:56:49 +0000 | nattkyrro | (~serenity@user/nattkyrro) (Quit: WeeChat 4.6.3) |
| 2026-04-25 11:53:47 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-25 11:47:10 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 11:44:15 +0000 | misterfish | (~misterfis@84.241.219.32) (Ping timeout: 246 seconds) |
| 2026-04-25 11:40:28 +0000 | <edwardk> | thirdofmay1808814goya: filtered (is _Foo) will imit a traversal to targets that pass match the _Foo prism, note this is technically an illegal traversal if you apply updates that change the fact that the prism matches, but no lens police will come for you. |
| 2026-04-25 11:36:09 +0000 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 245 seconds) |
| 2026-04-25 11:35:52 +0000 | orcus | (~orcus@user/brprice) brprice |
| 2026-04-25 11:35:22 +0000 | dispater | (~dispater@user/brprice) brprice |
| 2026-04-25 11:35:07 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-25 11:33:38 +0000 | orcus | (~orcus@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2026-04-25 11:33:38 +0000 | dispater | (~dispater@user/brprice) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2026-04-25 11:31:03 +0000 | dontdieych | (~dontdieyc@132.226.169.184) dontdieych |
| 2026-04-25 11:29:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-25 11:28:56 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-25 11:28:56 +0000 | arandombit | (~arandombi@2a02:2455:8656:7100:cc5a:dcbe:6803:acae) (Changing host) |