[CakeML] Hello CakeML'ers

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Fri Jun 13 13:15:31 UTC 2014


On Fri, Jun 13, 2014 at 2:29 AM, Andy Ray <andy.ray at ujamjar.com> wrote:

> Hi,
>

Hi Andy!


> I was recently told about CakeML during a visit to Cambridge Uni and
> have been meaning to have a proper look at it.  My interest is around
> uses of ML (actually more specifically OCaml) on FPGAs.
>

Excellent. Have you asked the OCaml community whether they already support
any FPGA backends? If so, I expect that would probably be the best route
for your interests. The focus for CakeML is full verification; if you're
not at all interested in verification then you'll be going through extra
hoops for nothing. That said, we also want CakeML to be a usable and useful
implementation even when you don't care about verification. (It's not quite
there yet...)


> When I asked David Greaves about OCaml on FPGA he pointed out this
>
>
> http://technotes-djg.blogspot.co.uk/2013/08/tndjg0004-i-converted-my-processor.html
>
> As a starting point I wonder if you have any advice on how I could use
> the code at
>
> https://github.com/xrchz/vml
>
> to compile an OCaml program which could run on Davids processor model?
>

There are a few blockers at the moment to the above plan:

   1. CakeML is a subset of Standard ML, not OCaml. In particular we use
   the syntax of the former. There has been talk (and perhaps even a bit of
   work) towards supporting OCaml syntax as well (e.g. see the first item at
   https://cakeml.org/projects.html) but it is not currently supported.
   2. The version of CakeML Bytecode that David Greaves implemented is
   likely somewhat out of date - we would probably need to get back in sync
   with him if you want to use the latest version of the compiler. On a
   related note, the roadmap for CakeML involves shifting focus away from the
   bytecode in favour of a new backend with a more traditional series of back
   end languages. We hope the new backend might also be suitable for targeting
   FPGAs, or perhaps to support an alternative route to bytecode (which can
   then be implemented on FPGA), but the new backend is still work-in-progress.
   3. There are probably OCaml features you want to use that aren't (yet)
   supported in CakeML.
   4. The verified CakeML Bytecode implementation is not quite finished.

So, there's plenty to work on :) If you're still interested, we could talk
more about the details and what we would need to do to support your
applications.

Longer term I am interested in the possibility of implementing
> something like LWT-light on top of this CPU as a potential controller
> for FPGA related gubbins (serial port, network, etc).
>

Sounds cool.


> In the interests of full disclosure I have no real understanding of
> the theorem proving world, though I suspect I probably should.
>

If you're using CakeML it probably would make sense :)

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140613/8f536288/attachment.html>


More information about the Users mailing list