Newest at the top
| 2024-04-29 22:21:38 +0200 | <shapr> | :-) |
| 2024-04-29 22:21:31 +0200 | <tomsmeding> | some people working on egraphs and saying that they're good |
| 2024-04-29 22:21:15 +0200 | <tomsmeding> | e-graphs-good |
| 2024-04-29 22:21:11 +0200 | <tomsmeding> | it's an interesting way to do things, I hadn't thought about that |
| 2024-04-29 22:21:09 +0200 | <monochrom> | What is the egg group? |
| 2024-04-29 22:20:40 +0200 | <shapr> | probably :-) |
| 2024-04-29 22:20:23 +0200 | <tomsmeding> | a human looks at those discovered equivalences and thinks hard about whether they make sense? |
| 2024-04-29 22:20:20 +0200 | <shapr> | then it uses those to build an equivalence graph |
| 2024-04-29 22:20:08 +0200 | <tomsmeding> | and then? |
| 2024-04-29 22:20:01 +0200 | <tomsmeding> | I see |
| 2024-04-29 22:19:59 +0200 | <shapr> | yup |
| 2024-04-29 22:19:56 +0200 | <tomsmeding> | based on seeing whether your compiler produces the same output for them? |
| 2024-04-29 22:19:47 +0200 | <shapr> | brute force from what I read |
| 2024-04-29 22:19:44 +0200 | <shapr> | based on trying a bunch of things |
| 2024-04-29 22:19:38 +0200 | <tomsmeding> | based on what? :p |
| 2024-04-29 22:19:33 +0200 | <shapr> | I think in source programs |
| 2024-04-29 22:19:26 +0200 | <tomsmeding> | source programs? target programs? |
| 2024-04-29 22:19:21 +0200 | <tomsmeding> | equivalences in what |
| 2024-04-29 22:19:13 +0200 | <shapr> | the egg group has a tool that discovers equivalences for you |
| 2024-04-29 22:19:08 +0200 | <tomsmeding> | if you have semantics (interpreters) for source and target languages you can do model testing (a subset of PBT), i.e. generate source programs and test that interpret_src == interpret_tgt . compile |
| 2024-04-29 22:18:18 +0200 | <tomsmeding> | maybe if your languages are easy toy languages writing an interpreter for them is easy |
| 2024-04-29 22:17:55 +0200 | <tomsmeding> | which is not much easier than writing a compiler in the first place |
| 2024-04-29 22:17:45 +0200 | <tomsmeding> | but then you need to define full semantics again |
| 2024-04-29 22:17:32 +0200 | <tomsmeding> | s/, and an external proof that/and then test that/ |
| 2024-04-29 22:17:23 +0200 | <tomsmeding> | er |
| 2024-04-29 22:17:17 +0200 | <tomsmeding> | you mean an equivalence relation on source programs, one on target programs, and an external proof that if S1 ~ S2 && semantics(S1) == semantics(T1) && semantics(S2) == semantics(T2) then also T1 ~ T2? |
| 2024-04-29 22:17:12 +0200 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-04-29 22:16:04 +0200 | <shapr> | but that's not so useful because you already have eq-sat :-( |
| 2024-04-29 22:15:56 +0200 | <shapr> | If you had equivalance saturation floating around you could check that the compiler produces something in the output of eq-sat |
| 2024-04-29 22:15:20 +0200 | <tomsmeding> | of what? |
| 2024-04-29 22:15:15 +0200 | <shapr> | can you pull in equivalence relations? |
| 2024-04-29 22:15:09 +0200 | <tomsmeding> | you can only test certain components |
| 2024-04-29 22:14:43 +0200 | <tomsmeding> | so that's not helpful |
| 2024-04-29 22:14:36 +0200 | <tomsmeding> | which is essentially another compiler |
| 2024-04-29 22:14:30 +0200 | <tomsmeding> | because a compiler is fundamentally about translating between representations, so to do any large-scale property testing there you have to have a semantics for both your source and your target language, as well as a link between them |
| 2024-04-29 22:14:21 +0200 | Square3 | (~Square4@user/square) |
| 2024-04-29 22:13:57 +0200 | <tomsmeding> | but that's not even my point, even assuming you can do that there is not a whole lot to property-test |
| 2024-04-29 22:13:47 +0200 | <tomsmeding> | it's surprisingly difficult to generate _useful_ AST pieces (there was a paper at one of the major PL conferences about that last year, I can look it up if you want) |
| 2024-04-29 22:13:09 +0200 | <shapr> | Is it because it's difficult to generate AST pieces? |
| 2024-04-29 22:13:09 +0200 | <tomsmeding> | but that's mostly it |
| 2024-04-29 22:13:06 +0200 | <tomsmeding> | you can roundtrip-test a parser, if can generate valid syntax, and you can do some property testing of optimisations or subroutines of optimisations if you're lucky |
| 2024-04-29 22:12:58 +0200 | <shapr> | I've never tried testing a compiler, why doesn't it lend itself to that? |
| 2024-04-29 22:12:34 +0200 | <tomsmeding> | I've asked about this here before, but I find it somewhat awkward that we PL people say that property tests are great, but the standard PL example (compilers) doesn't lend itself very well for property testing |
| 2024-04-29 22:12:19 +0200 | <shapr> | My goal is to compare coverage driven testing to existing test suites, so I'd like to hear about any projects with a big pile of PBT |
| 2024-04-29 22:12:04 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:90bc:b4a5:eea5:19e6) |
| 2024-04-29 22:11:55 +0200 | <tomsmeding> | the code I write is typically compiler-y so it has the same situation :p |
| 2024-04-29 22:11:28 +0200 | <shapr> | do you have any other suggestions? |
| 2024-04-29 22:11:26 +0200 | <Rembane> | shapr: Lovely! |
| 2024-04-29 22:11:24 +0200 | <shapr> | that's a good point |
| 2024-04-29 22:11:18 +0200 | <tomsmeding> | the fact that it uses a property testing _framework_ notwithstanding |