opencascade.js VS Kind

For proper CAD in browser, you'd need something like opencascadejs. I've integrated it to Polygonjs, here is an example scene, and a video intro

That confirms the impression I had, I guess they are just so complex that building a new open source one from scratch would be Herculean effort. Guess OCCT is the only option for now.

The itch I would love to scratch is an online real-time collaborative parametric cad app using CRTDs. Current thinking is combining OpenCascade compiled to WASM [0] with Yjs[1], but frankly don’t have the time.

0: https://github.com/donalffons/opencascade.js/

1: https://github.com/yjs/yjs

Can I access a library that is compiled to WASM (e.g. openCascade.js) directly from a rust client web app that runs in the browser? The library is lgpl so I'd want to "dynamically link" to it.

As a developer of a proof assistant (Kind) I'm highly interested in this line of work. Can you point me to some of these papers? And perhaps people involved in this line of work?

Kind: A modern proof language (though functional).

I have seen in languages like KindLang the definition of Array be like a Binary tree, but there is some magic there in the definition of the Array type that I don't understand yet. Also, I don't want to define the contiguous array further., it should be a literal contiguous array. The Kind "Word" type definition (arbitrary number of bytes) is closer to my contiguous array, but it has a similarly complex definition which like I said I don't understand.

Totally agree about the Blub Paradox, but there's definitely value in Self Types. See, for example, [Kind](https://github.com/Kindelia/Kind), which is able to type recursive data types by using Self Types.

For these who don't know, I'm the author of Kind and HVM. I've recently seen a criticism from an influent person in the community, who I often took as an inspiration, that made me really sad. "the guy behind this has built some impressive-sounding stuff before... it looks like his projects tend to just... go nowhere and he just abandons them and does something else?"

This is very easy with dependent types! For example, in Kind: