Somehow the final version of the paper is not linked from the blog post: https://www.microsoft.com/en-us/research/publication/specifi...
87 karma · joined February 27, 2014
And we're not opposed to choice trees. I personally am not too familiar with them but there's time to catch up on literature. :)
My usual intuition is whether the generated code at the end needs a complicated runtime to replicate the source language's semantics. In Crane, we avoid that requirement with smart pointers, for example.
Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.
And we are looking for senior researchers to join us, see https://x.com/jvanegue/status/2004593740472807498
The output you posted is from an example that we missed importing. It's also one of the tests that do not yet pass. But then again, in the readme, we are upfront with these issues:
> Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker.
I should also note, mapping Rocq types to ideal C++ types is only one part of it. There are still efficiency concerns with recursive functions, smart pointers, etc. This is an active research project, and we have plans to tackle these problems: for recursion: try CPS + defunctionalization + convert to loops, for smart pointers: trying what Lean does (https://dl.acm.org/doi/10.1145/3412932.3412935), etc.
But Kip lets you repeat cases in arguments, so you're not limited to 8 arguments for a function. In cases where a function takes multiple arguments of the same case, the order in which those arguments are applied matters, otherwise it doesn't. So if you say "any number of arguments but only 8 are named, that seems bad", I'd understand, but that is a relatively uncommon problem to run into, especially in a toy language like this that is not meant for any serious work.
(5'in mutlak-değerini) yaz.
(-5'in mutlak-değerini) yaz.
You can try it in the playground.
If it helps, you can think of it like named arguments where the name is inferred from the case.
My solution for this problem in Kip was to go all the way with the morphological analysis using TRmorph (https://github.com/coltekin/TRmorph) for it, and then resolve the ambiguities in type checking / elaboration. (Therefore Kip almost never needs apostrophes.) Whether it was worth it, I don't know, but it was a fun problem to solve. :)
(The work on JavaScript transpilation just started today and currently doesn't work, but running the language should mostly work, though it probably has bugs, which I'd love to hear about in the repo's issues!)