Kind2 VS sdl-gpu-hs

Agreed. Even from a PLT perspective, I prefer Kind2 by the Kindelia Foundation for supporting inductive theorem proving (and hopefully some level of dependent types), as well as being faster to boot.

I agree. Keep in mind our language (Kind-Lang) does target the HVM, and it is really promising. The type-checker is the fastest among proof assistants, by far; the error messages are really nice; it has a fully dependent type system which is a breath of fresh air to work with. It is still not production ready though (mostly due to lack of IO), but is the extend of our effort on that direction. We hope other lang developers get encouraged to target the HVM to. Elm and Idris are great candidates for that IMO.

Another very small proof system: https://github.com/moonad/formcorejs

The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js

The author has since moved on to building a runtime with optimal evaluation (https://github.com/kindelia/hvm) and a new proof language on top of that (https://github.com/Kindelia/Kind2) with considerably better performance than existing proof systems.

The bindings are currently source-only here. I am going to release to Hackage soon (tm), but I just haven't had the time to button it up. However, they do work great. Every game I've done for Ludum Dare except 47 (which was gloss) has used these bindings.

The guts are in the Memorable module. There are some operators in there that allow you to pluck individual fields from struct pointers in IO instead of marshaling entire structs needlessly.

The games are built on a custom "engine" made with SDL2 and some other C libraries I wrote bindings for: sdl-gpu, cute_c2, and cute_sound. I use apecs and cleff for the general architecture. And for animations, I use a combination of animate and ease.

You can't exactly allocate data in this custom memory management system, but you can get close with some type-level/generics stuff I think. I've been playing with it quite a bit for no-marshal hsc FFI bindings [1] [2], and it's worked nicely for that in raw IO. With some extra elbow grease, I can probably make it work for pure linear code too.