Our great sponsors
-
Functional-Benchmarks
Collection of benchmarks of functional programming languages and proof assistants.
-
SurveyJS
Open-Source JSON Form Builder to Create Dynamic Forms Right in Your App. With SurveyJS form UI libraries, you can build and style forms in a fully-integrated drag & drop form builder, render them in your JS app, and store form submission data in any backend, inc. PHP, ASP.NET Core, and Node.js.
Earlier this year, I've released the first version of HVM, a massively parallel functional runtime that aims to be the ultimate target for pure functional languages like Haskell, Elm, Kind and many others. Its main goals are to 1. be beta-optimal, which has applications on the complexity of functional algorithms, and, 2. to fully unleash the inherent parallelism of functional programming, and run programs in thousands of cores. HVM's first parallel version was very limited; it could only parallelize algorithms that recursed in a perfect binary tree fashion, and it had a synchronization bug. Soon, we'll be releasing an updated version, which fixes these bugs, and includes a new work-stealing-based scheduler, which is capable of generalizing to basically any functional program that isn't inherently sequential. For example, it can use all cores on the computation of Fib(n), achieving maximal performance. This was simply not possible before.
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.
Have you considered FIR for generating Vulcan shaders to hand off to GPUs?
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.