| 9 Nov 2024 |
 finlifin | 🐧 | 08:19:08 |
 everett.hildenbrandt | Yep! In fact, one of the tools you get is a verification engine based on symbolic execution! | 15:43:39 |
| everett.hildenbrandt | What are you thinking to build? | 15:43:45 |
| 10 Nov 2024 |
| finlifin | oh | 05:28:49 |
| finlifin | i am exploring a new asynchronous programming paradigm and semantics based on transactional memory and concurrent program verification | 05:30:32 |
| 11 Nov 2024 |
| everett.hildenbrandt | Well, K can definitely be used to model that! It's good at handling concurrency and distributed systems! | 01:01:16 |
| finlifin | and how does k verify separation logic assertions 👀 | 09:14:28 |
 raoul.schaffranek | The K-Framework is based on Matching Logic, which can be viewed as a generalization of separation logic. This should be a good starting point: https://research.runtimeverification.com/#separation-logic-in-matching-logic | 09:48:33 |
| finlifin | love you | 09:52:13 |
| finlifin | lol | 09:52:15 |
| 14 Nov 2024 |
| finlifin | how does k due with the verification programs that contains reference aliasing | 01:14:32 |
| finlifin | * how does k due with the verification of programs that contains reference aliasing | 01:14:48 |
| finlifin | my programming language does have an ownership type system to ensure there's no aliasing | 01:19:00 |
| finlifin | 🤧 | 01:19:07 |
| finlifin | * my programming language does not have an ownership type system to ensure there's no aliasing | 01:20:26 |
| 20 Nov 2024 |
| everett.hildenbrandt | It certainly can be modelled, the question is whether reasoning about it will be easy or not. K does not make any assumptinos about how your programming language works, so you can model whatever system you want. In the C semantics, for example, we fully module the C17 standard and that includes the possibility of undefined behavior and pointer aliasing: https://github.com/kframework/c-semantics | 01:43:56 |
| everett.hildenbrandt | Unlike other logical frameworks (like separation logic), we do not commit to a particular way of representing memory/heap, we let the user model it how they like out of the primitive ADTs and functional sub-language that K provides. | 01:44:28 |
| 5 Dec 2024 |
|  Andrew Helwer joined the room. | 19:54:38 |
| Andrew Helwer | Hello! Recently learned about K and it looks very interesting. One question I have: once you've specified your language's syntax and semantics in K, is it possible to use it to generate arbitrary semantically-valid files for your language? So then K could function as a fuzzing oracle for other implementations of your language. | 19:58:29 |
| Andrew Helwer | A second question I have is how the K parsing language handles non-context-free parts of languages, for example Python's indentation-sensitive syntax. The language I am involved in (TLA+) has something similar with vertically-aligned conjunction and disjunction lists. | 19:59:24 |
| everett.hildenbrandt | Generating syntactically valid programs is definitely possible. Semantically valid depends on the definition of that, you would need a typing semantics to generate type valid programs, and you could reasonably generate ones valid for execution by using the execution semantics. You could also reverse the rules of a semantics and potentially generate new programs that way, though that would be pretty experimental. | 20:44:09 |
| everett.hildenbrandt | Non-context-free is possible to an extent Ks parser is pretty powerful and you can control a lot of aspects of it. But for real language use, you usually want to use an external parser which then spits out ASTs for K to use, because a dedicated parser will be faster usually. | 20:45:34 |
| Andrew Helwer | Thanks! So to be clear by possible it isn't as simple as plug a K spec into an existing tool, this would be a research project? | 20:49:25 |
| everett.hildenbrandt | It would require a bit of python scripting to get syntactically valid programs, and a bit more to check that they're valid for execution (don't get stuck), and would require a typing semantics (usually smaller than an execution semantics) to generate type valid programs. So I wouldn't say it's a research project (all the steps are clear), but would require some engineering work. | 20:54:18 |
| Andrew Helwer | For the valid type-level programs would those also follow the generate-syntax-and-test method or are they build constructively? | 20:56:19 |
| Andrew Helwer | (TLA+ has a very simple pseudo-type system where we just categorize expressions into constant, state-level, action-level, or behavior-level) | 20:57:00 |
| everett.hildenbrandt | Generate syntaxes then test approach is where I would start. As an experiment, you can try reversing the rules in a semantics and then using that to generate programs in a given type. That would probably be a bit more direct of a way to generate type-valid programs, but would be more experimental. Pyk (the python library for k definitions) would make that procedure easier. | 21:09:39 |
| 6 Dec 2024 |
|  David | W3F - Zug 9 - 13 Dec. changed their display name from David | W3F to David | W3F - OOO (sick). | 06:23:28 |
| 9 Dec 2024 |
| David | W3F - Zug 9 - 13 Dec. changed their display name from David | W3F - OOO (sick) to David | W3F. | 07:52:14 |
| 10 Dec 2024 |
| David | W3F - Zug 9 - 13 Dec. changed their display name from David | W3F to David | W3F - Zug 9 - 13 Dec.. | 06:53:42 |
