1. 8
    1. 1

      I’ve been collecting resources for automating verification and/or synthesis of programs. Although plenty exist for data, there’s a lot less for control flow. They usually need some clean or at least precise way to specify it that a mechanical translation handles from there. I’m surprised I haven’t seen recursion schemes before this post since it superficially looks like it would help there. Maybe it could be built on CakeML or something.

      1. 3

        Have you read Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire? I guess you might be interested in a more lang-neutral formalism of this same concept.

        1. 1

          Thanks for the link. :)

          1. 5

            This may also be helpful while going through that paper: http://blog.ezyang.com/2010/05/bananas-lenses-envelopes-and-barbed-wire-a-translation-guide/

            (Although, it brings it back into the Haskell domain, but still may be more comprehensible than some of the notation in that paper…)