HackerTrans
TopNewTrendsCommentsPastAskShowJobs

meghprkh

no profile record

Submissions

Creating Rust macros with crabtime for including icons in Leptos

meghprkh.github.io
5 points·by meghprkh·letztes Jahr·0 comments

Rust Traits – Associated Types and Generic Traits

meghprkh.github.io
2 points·by meghprkh·letztes Jahr·0 comments

comments

meghprkh
·letzten Monat·discuss
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)
meghprkh
·vor 2 Monaten·discuss
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 )
meghprkh
·letztes Jahr·discuss
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.
meghprkh
·letztes Jahr·discuss
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!