Newest at the top
| 2026-02-07 14:20:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-02-07 14:19:04 +0100 | <[exa]> | mesaoptimizer: might be way easier to just fix the error than try to explain it to a mechanical parrot |
| 2026-02-07 14:18:31 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2026-02-07 14:15:39 +0100 | ZLima12 | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2026-02-07 14:15:14 +0100 | ZLima12 | (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2026-02-07 14:14:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 14:11:45 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2026-02-07 14:03:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-07 14:00:58 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) |
| 2026-02-07 13:59:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:59:08 +0100 | trickard_ | trickard |
| 2026-02-07 13:56:14 +0100 | Square2 | (~Square@user/square) Square |
| 2026-02-07 13:48:39 +0100 | <mesaoptimizer> | int-e: recommended reading to understand SMT solvers? |
| 2026-02-07 13:48:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 13:47:55 +0100 | emmanuelux | (~em@user/emmanuelux) (Quit: bye) |
| 2026-02-07 13:46:17 +0100 | <mesaoptimizer> | gentauro: I'm trying to patch microhs / mcabal using Gemini 3 Pro to be able to build `http-conduit`, and I must say, I'm not impressed |
| 2026-02-07 13:45:19 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2026-02-07 13:44:23 +0100 | <mesaoptimizer> | jreicher: I am on #emacs but never read it |
| 2026-02-07 13:43:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:40:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-07 13:37:14 +0100 | Pozyomka | (~pyon@user/pyon) pyon |
| 2026-02-07 13:35:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:32:26 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-02-07 13:32:25 +0100 | comonad | (~comonad@pd9e072e5.dip0.t-ipconnect.de) |
| 2026-02-07 13:31:41 +0100 | Pozyomka | (~pyon@user/pyon) (Quit: WeeChat 4.8.1) |
| 2026-02-07 13:30:14 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-02-07 13:26:10 +0100 | comonad | (~comonad@p200300d02722ae00dce4ce9451b59974.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-02-07 13:23:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 13:17:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 13:06:59 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:06:07 +0100 | jreicher | (~joelr@user/jreicher) (Remote host closed the connection) |
| 2026-02-07 13:06:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 13:05:22 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-02-07 13:00:30 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-02-07 12:58:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:55:07 +0100 | <ski> | (i was recently starting to formulate (optimized) CPS-transformation, first in lambdaProlog (which also has matching on HOAS, but not dependent types), then trying to do it in Twelf, for comparision .. ran out of steam, after a while, fighting with it to accept some parts, though) |
| 2026-02-07 12:53:45 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-07 12:50:53 +0100 | <ski> | .. i can't keep from feeling like there ought to be a way to address those concerns more directly .. rather than resorting to going to a different (functional) computational model. Twelf is the only dependently typed logic programming language i'm aware of, and it would seem to be a shame to not further develop that |
| 2026-02-07 12:50:36 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) |
| 2026-02-07 12:49:25 +0100 | <ski> | the issue being limitations in reasoning about local parameters (data constructors), and local assumptions, for the mode-checking. and, perhaps, also some limitations in doing (effectively) anonymous predicates, e.g. extending an accumulator predicate parameter -- and associated reasoning about mode for such higher-order predicates |
| 2026-02-07 12:47:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-02-07 12:47:13 +0100 | <ski> | said above (meta-)proof checking) |
| 2026-02-07 12:47:06 +0100 | <ski> | one of the reasons they stated for developing Delphin (rather than Twelf), was a claim of having trouble with some kinda of higher-order programming. afaict, what they mean by this is not lack of support for higher-order predicates, per se, but rather lack of adequate support for the static mode&determinism *checking* (which is optional (from a computational standpoint), but essential for when you want to do |
| 2026-02-07 12:46:32 +0100 | Beowulf | (florian@2a01:4f9:3b:2d56::2) (Quit: = "") |
| 2026-02-07 12:44:18 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-02-07 12:42:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 12:35:26 +0100 | <ski> | it also has facilities to be able to state such theorems, and let a theorem-prover (in the language implementation) search for a proof (and realize it as a recursive predicate) |
| 2026-02-07 12:34:27 +0100 | <ski> | so, the system has facilities to do this (meta-proof) checking of modes, in order to ensure that the predicate whose definition encodes your proof actually proves the intended thing (e.g. that if an (object-language) term has some type, and you reduce the term one step, then it still has that type) |
| 2026-02-07 12:33:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-02-07 12:32:43 +0100 | <ski> | mode&determinism declaration on the predicate (if you will, ensuring that the relation is functional) |