meghprkh

I would like such a project in Rust! There a bunch of embassy-based firmwares but none have the UX of the crosspoint forks yet. My favourite is inx (https://github.com/obijuankenobiii/inx) which is the only one that supports annotations afaik. It does crash sometimes though

Not necessarily. Since the word "typed" language is not well-defined.

For example, typescript is a fantastic language for marshalling data and UI state since it uses substructural typing instead of nominal typing. Libraries like kysely / other ORM libraries are great examples too and easy to use, whereas in fully typed languages like Rust you would end up having to use a macro library like sqlx or having to define structs for each of your types (which would increase compile time & size)

Why would they not do something like?

  + #if !(defined __GLIBC_COMPILER_SUPPORTS_ATTRIBUTES__)
  - #if !(defined __GNUC__ || defined __clang__ || defined __TINYC__)
  # define __attribute__(xyz)     /* Ignore */
  #endif

(or probably a more fine grained for each attribute they try to use)

Considering such checks are fairly conventional in downstream C++ libraries based on compilers (for example checking OS platform or compiler, e.g. [Boost.Config](https://www.boost.org/doc/libs/latest/libs/config/). Modern C++ even went ahead and standardized this somewhat https://en.cppreference.com/cpp/utility/feature_test )

No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think.

What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?

Because from what I understand Rocq too has Gallina or something right?

I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.

What is the real difference between rocq vs lean? Alternatively, what is your motivation to do this in lean as compared to playing around with the rocq one if it exists?

I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!

C++20 Concepts are a new language feature that ease generic programming, but are primarily syntactic sugar.

We will try to implement them in C++03, with one caveat - we must explicitly specify that a class implements an concept.

NOTE: We will use template specialization and do not need to be able to modify the class or our concept for this.