Newest at the top
2025-07-31 12:02:34 +0200 | caubert | (~caubert@user/caubert) (Ping timeout: 260 seconds) |
2025-07-31 11:59:19 +0200 | inline | (~inline@ip-005-146-197-054.um05.pools.vodafone-ip.de) Inline |
2025-07-31 11:58:32 +0200 | VictorHugenay | (~VictorHug@user/VictorHugenay) VictorHugenay |
2025-07-31 11:57:09 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 248 seconds) |
2025-07-31 11:56:39 +0200 | dextaa | (~dan@user/dextaa) dextaa |
2025-07-31 11:55:07 +0200 | jackdk | (uid373013@cssa/life/jackdk) (Quit: Connection closed for inactivity) |
2025-07-31 11:50:41 +0200 | <mauke> | non-terminating, but productive |
2025-07-31 11:50:06 +0200 | <kuribas> | The whole loop is not total, but the input -> result part is total. |
2025-07-31 11:49:56 +0200 | <__monty__> | There's the rub, isn't it? |
2025-07-31 11:49:35 +0200 | <kuribas> | The important part is of course that you get results with bounded fuel. |
2025-07-31 11:48:59 +0200 | <kuribas> | Then in practice you run with infinite fuel. |
2025-07-31 11:48:52 +0200 | <kuribas> | __monty__: you use fuel. You just run the deamon as long as there is fuel. |
2025-07-31 11:46:49 +0200 | inline_ | (~inline@ip-005-146-197-054.um05.pools.vodafone-ip.de) (Quit: Leaving) |
2025-07-31 11:45:19 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
2025-07-31 11:44:57 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) |
2025-07-31 11:41:00 +0200 | Digit | (~user@user/digit) (Ping timeout: 276 seconds) |
2025-07-31 11:39:16 +0200 | tromp | (~textual@2001:1c00:3487:1b00:b928:de3f:1dfd:983a) |
2025-07-31 11:35:44 +0200 | trickard_ | (~trickard@cpe-54-98-47-163.wireline.com.au) |
2025-07-31 11:35:30 +0200 | trickard | (~trickard@cpe-54-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
2025-07-31 11:34:15 +0200 | <apache2> | but if you can write the inner loop as a step that you can prove termination for, then you can have a small runner, and you know the inner loop won't get stuck |
2025-07-31 11:32:59 +0200 | <apache2> | __monty__: I guess if you can prove things about the inner loop, you can often prove that the program doesn't terminate |
2025-07-31 11:31:31 +0200 | <__monty__> | As soon as you have something long running like a daemon or a GUI, termination checking sounds like it should get hard to me. |
2025-07-31 11:31:21 +0200 | <apache2> | I don't know about trivial, in languages where you can ask the type checker to check that your functions are total (like Agda) it's often *not trivial* to convince the type checker that that's the case |
2025-07-31 11:30:19 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Ping timeout: 272 seconds) |
2025-07-31 11:30:14 +0200 | <apache2> | it can still be a practical program, UNIX "yes" is an example of such |
2025-07-31 11:29:43 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Remote host closed the connection) |
2025-07-31 11:29:35 +0200 | <apache2> | kuribas: in python you can write a program `while True: print("SPAM")` which clearly does not terminate |
2025-07-31 11:28:34 +0200 | <apache2> | it's a definition game |
2025-07-31 11:28:17 +0200 | <apache2> | segfaults leading to program termination is usually not, but you could define a language where that is a valid outcome |
2025-07-31 11:28:06 +0200 | <kuribas> | I just think most practical programs are trivially total. |
2025-07-31 11:26:32 +0200 | <apache2> | kuribas: throwing an exception is usually considered progress. |
2025-07-31 11:25:54 +0200 | <apache2> | kuribas: it's better if your aim is to prove things about the results :) it may not be better if your goal is to write a program that performs the task at hand - the more complicated the type system, the less likely the programmer is to terminate :) |
2025-07-31 11:25:40 +0200 | <kuribas> | An that any expression can throw any exception. |
2025-07-31 11:25:22 +0200 | <kuribas> | progress also disregards exceptions in many language, no? |
2025-07-31 11:24:11 +0200 | <__monty__> | It's interesting at least. |
2025-07-31 11:23:35 +0200 | <kuribas> | So total programming is better... |
2025-07-31 11:23:20 +0200 | <apache2> | which is a hell of a lot better than "yolo" but it doesn't mean your program will do what it was intended to do |
2025-07-31 11:22:51 +0200 | <apache2> | but if you can't prove that functions terminate, it's hard to talk about codomains. then you end up with "iff the function terminates, the result has the correct type" |
2025-07-31 11:21:28 +0200 | <apache2> | kuribas: sure, ensuring domains+codomains match up is a useful and common thing to achieve in a type checker |
2025-07-31 11:21:11 +0200 | caubert | (~caubert@user/caubert) caubert |
2025-07-31 11:20:52 +0200 | <apache2> | ie you may be able to rule out stalling Progress due to Int<->Float mismatch, but you may not be able to rule out stalling due to unterminating functions |
2025-07-31 11:20:27 +0200 | <kuribas> | Couldn't you say that it is about making sure the domains of functions are respected? |
2025-07-31 11:18:54 +0200 | <apache2> | type checking is usually used to verify that the program is internally consistent, not that it works. "internally consistent" is also a fluid concept, "with respect to which properties" is the follow-up question you can ask, and that the operational semantics should answer |
2025-07-31 11:18:21 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
2025-07-31 11:17:23 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
2025-07-31 11:16:49 +0200 | <kuribas> | Or a static analyser that shows some expression always throws a type error. |
2025-07-31 11:16:10 +0200 | <kuribas> | like with gradual typing you could have the properties failing... |
2025-07-31 11:15:58 +0200 | <kuribas> | true |
2025-07-31 11:15:43 +0200 | <apache2> | "dynamic" and "static" are fluid concepts, I'd be wary of treating conjectures that talk about "dynamic programming languages" as formal conjectures |
2025-07-31 11:15:40 +0200 | merijn | (~merijn@77.242.116.146) merijn |