2025/07/31

Newest at the top

2025-07-31 12:02:34 +0200caubert(~caubert@user/caubert) (Ping timeout: 260 seconds)
2025-07-31 11:59:19 +0200inline(~inline@ip-005-146-197-054.um05.pools.vodafone-ip.de) Inline
2025-07-31 11:58:32 +0200VictorHugenay(~VictorHug@user/VictorHugenay) VictorHugenay
2025-07-31 11:57:09 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 248 seconds)
2025-07-31 11:56:39 +0200dextaa(~dan@user/dextaa) dextaa
2025-07-31 11:55:07 +0200jackdk(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 +0200inline_(~inline@ip-005-146-197-054.um05.pools.vodafone-ip.de) (Quit: Leaving)
2025-07-31 11:45:19 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-07-31 11:44:57 +0200sprout(~sprout@84-80-106-227.fixed.kpn.net)
2025-07-31 11:41:00 +0200Digit(~user@user/digit) (Ping timeout: 276 seconds)
2025-07-31 11:39:16 +0200tromp(~textual@2001:1c00:3487:1b00:b928:de3f:1dfd:983a)
2025-07-31 11:35:44 +0200trickard_(~trickard@cpe-54-98-47-163.wireline.com.au)
2025-07-31 11:35:30 +0200trickard(~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 +0200LainIwakura(~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 +0200sprout(~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 +0200caubert(~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 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-07-31 11:17:23 +0200Frostillicus(~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 +0200merijn(~merijn@77.242.116.146) merijn