awesome-rust-formalized-reasoning VS Kind

Unsurprisingly, we can see a growing interest in the Rust ecosystem regarding formal verification. I try to keep https://github.com/newca12/awesome-rust-formalized-reasoning up to date. I will add CreuSAT shortly.

This dispersed progress is the sign of an absence of maturity but the exploration of this space with Rust is very promising : https://github.com/newca12/awesome-rust-formalized-reasoning

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.

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?"

I really like the idea of ownership and ownership types / affine types, which it seems like the borrow checker implements (for garbage collection features and the general type theory benefits you get). Though I am no type theory expert, just been browsing around trying to figure out how the ideal compiler would work, finding things like lobster lang and kind lang along the way.

The plan for Kind itself seems to be to allow possibly unsound expressions (for example that don’t terminate), but to have consistency checkers. See:

https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...