Kind VS fornjot

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:

I agree 100%.

Truck[1] and Fornjot[2] are recent attempts in the Rust space, both are WIP.

But both seem to be going the traditional way. I.e. B-Rep that can be converted to (trimmed) NURBS.

I think if one wanted to incorporate the last 50 years of computer science, particularly computer graphics, one needed to broaden the feature set considerably.

You need support for precision subdivision surface modeling with variable radius creases (either via reverse subdivision where you make sure the limit surface pass through given constraints or using an interpolating subivision scheme that but has the same perks as e.g. Catmull-Clark).

Then you need to have SDF modeling ofc.

Possibly point based representations. If only as inputs.

And traditional B-Rep.

Finally, the kernel should be able to go back and forth lossless between these representations wherever possible.

And everything must be node-based, like e.g. Houdini. Completely non-destructive.

[1] https://github.com/ricosjp/truck

[2] https://github.com/hannobraun/fornjot

Fornjot seems like this question was tailored for it: https://www.fornjot.app/

I think some interesting developments are made in that sector in the form of https://github.com/hannobraun/Fornjot and https://github.com/ricosjp/truck. Let's see whether one of those will actually get anywhere near a usable level. Fornjot in particular is shaping up really well.

E.g. Rhai[2] or Lua or whatever.

And I guess if their tech is solid enough, someone will do that eventually and open a PR or fork the project. They do not use an existing geomtry kernel but do everything from scratch which makes this a very interesting endeavour.

There also seems to be a goal overlap between Fornjot and DieselCAD

[1] https://github.com/hannobraun/Fornjot

[2] https://rhai.rs/

I have heard of yet another in-development CAD software like OpenSCAD or CADQuery, called Fornjot. Still, these are not ideal.

I'm not opposed to someone else adopting that code and creating that crate though! (Fair warning though, Fornjot might not end up using that crate. We might still go with another approach eventually.)

also it's to early to be off much use to you, but have you heard of https://www.fornjot.app/ ? it's a very in development cad kernel that is also aiming for integration into multiple host languages.

Yes! The website and repository README have a screenshot, and there are screenshots for each model in the models/ directory.

I'm kind of interested in this issue because it's what I immediately wanted when I ran fj-app.