Newest at the top
| 2025-05-04 14:35:31 +0200 | <[exa]> | and yeah well it's actually prolog. I want to write constraints on what holds "before" and should hold "after" the program, and the thing would ideally fill in some "middle" so that the "after" is satisfied. |
| 2025-05-04 14:35:19 +0200 | <haskellbridge> | <hellwolf> I think the hvm person is doing this entire neogen thing, banking on LLM model. |
| 2025-05-04 14:32:31 +0200 | <[exa]> | tomsmeding: I've just started reading up on the whole topic. Looks like I wanted more of a program synthesis. :D |
| 2025-05-04 14:31:23 +0200 | <[exa]> | hellwolf: if the heuristic is "there was more chat about it on the internet", it's going great. |
| 2025-05-04 14:26:50 +0200 | <haskellbridge> | <hellwolf> I wonder how well LLM nowadays to cope with these sort of things when it comes to heuristics |
| 2025-05-04 14:22:24 +0200 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |
| 2025-05-04 14:21:47 +0200 | <tomsmeding> | what kind of things do you want to prove? |
| 2025-05-04 14:21:16 +0200 | <tomsmeding> | I mean you can actually model a proof checker, but at that point you're writing what you're asking already exists, I guess :p |
| 2025-05-04 14:16:02 +0200 | <[exa]> | s/List/Logic/ |
| 2025-05-04 14:15:19 +0200 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 2025-05-04 14:14:12 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-04 14:11:57 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 14:05:46 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 14:04:14 +0200 | <tomsmeding> | prolog? |
| 2025-05-04 14:01:26 +0200 | <[exa]> | the issue with the theorem provers I see is that they kinda assume some particular fixed algebra (some kind of logic), I need some freedom in there without having to encode stuff too much. |
| 2025-05-04 13:58:47 +0200 | <[exa]> | s/if // |
| 2025-05-04 13:58:36 +0200 | <[exa]> | are there some good "small" libraries theorem proving? E.g. I've got an algebra, a few axioms on it, and I want to see how the axioms can be combined to derive some expression in the algebra. Ideally if axiom schemes are supported. |
| 2025-05-04 13:52:15 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 13:51:45 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 13:51:28 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 13:45:09 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 13:38:10 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 13:25:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 2025-05-04 13:16:15 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2025-05-04 13:13:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-05-04 13:08:16 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 13:07:59 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 13:07:29 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-05-04 13:00:43 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 12:53:03 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 12:52:13 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 265 seconds) |
| 2025-05-04 12:45:48 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 12:38:34 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-05-04 12:36:50 +0200 | <hellwolf> | I wish the docs actually care to give just a few lines of "why". But I guess it risks of being too brief and confuses some people. Not sure what's the good middle ground of these sort of things is. |
| 2025-05-04 12:33:27 +0200 | <Rembane> | That sounds neat |
| 2025-05-04 12:31:27 +0200 | <hellwolf> | I watched it. TL;DV: to index optical operations into one type class, so that you can stack them up in your application monad. It's probably obvious if you actually build such a application that deal with real world :) |
| 2025-05-04 12:27:57 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-05-04 12:16:50 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:15:17 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 2025-05-04 12:14:42 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-05-04 12:05:04 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 2025-05-04 12:04:37 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 12:00:10 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 11:51:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 11:47:19 +0200 | Square | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-05-04 11:37:12 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-04 11:22:22 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-05-04 11:21:57 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-05-04 11:16:27 +0200 | <haskellbridge> | <hellwolf> thank you! checking now |
| 2025-05-04 11:13:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) |