[CakeML-dev] idris also facing the killer app question

[Magnus Myreen]

Thanks for the link.

My answer to this question is that CakeML is well suited for
applications that need high assurance (verification) and do a lot of
data processing where the data is variable in size (benefits from
automatic memory management) and represented as trees (good use of
pattern matching).

Examples in this area are:
 - theorem provers such as HOL / Candle
 - certificate checkers, static analysis tools, automatic provers (e.g. Daisy)
 - program transformers / compilers (also other than the CakeML compiler)

Cheers,
Magnus

On 21 April 2017 at 04:05, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> slightly off-topic, but maybe of interest. I think CakeML is (has been)
> asking this same question too ("CakeML is the best tool for ___?"):
> https://groups.google.com/forum/#!topic/idris-lang/xX5rUI1kKMM
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>