Finally, I can witness Tsoding's not coq

Made my day. Impressive to say Coq so many times and not get banned from YT :P

If you're interested in this (graph transformations and equivalence), you should definitely check out egg (E-Graphs Good) and E(quivalence)-Graphs in general (if you haven't already)! (It's written in Rust, so bear caution! ;) Gist: The basic idea is that you have your Abstract Syntax-DAG that contains your expression and you apply rules and what you get is your transformed expression *while keeping* the _original_ one in the *same* data structure, so that subsequent applications still have that information. So by applying all your rules again and again you eventually reach a state where potentially none match anymore (called saturation) and you have ALL POSSIBLE derivations, from which you can select your desired one.

Bug: Some bindings are left populated even if match fails. Bindings should only be filled if all arguments of a functor are matching, but are populated for each argument, even if later arguments do not match.

Всё правильно - не кок, а повар плавсостава. Спасибо за просвещение, Тсодинг Ежедневник.

1:02:30 One thing you can do to make the &str -> String conversion clearer is using `to_owned` instead of `to_string`; it does the exact same thing but it's clearer what the actual purpose of the method call is: to convert from a borrowed slice of another string to an independent "owned" string. The fact that `to_string` does the same thing is kind of just a coincidence, since it's just a trait method for any type that can be converted to a string.

Also definitely check out the logos crate, which is an uncomplicated lexer state-machine generator that provides you with a *really fast* (subset of) regex and token macros ontop of your Lexeme enum, so that you don't have to re-implement lexing all-the-time and can focus on parsing (we use it in out university's compilers class as a rust alternative to (f)lex). It can be a bit rough around the edges (no lookahead or non-greedy matching, and the documentation isn't the best) but provides easy workarounds for the nitty-gritty and should be completely sufficient for your use-case. (I am not affiliated)

No Porth? ⠀⣞⢽⢪⢣⢣⢣⢫⡺⡵⣝⡮⣗⢷⢽⢽⢽⣮⡷⡽⣜⣜⢮⢺⣜⢷⢽⢝⡽⣝ ⠸⡸⠜⠕⠕⠁⢁⢇⢏⢽⢺⣪⡳⡝⣎⣏⢯⢞⡿⣟⣷⣳⢯⡷⣽⢽⢯⣳⣫⠇ ⠀⠀⢀⢀⢄⢬⢪⡪⡎⣆⡈⠚⠜⠕⠇⠗⠝⢕⢯⢫⣞⣯⣿⣻⡽⣏⢗⣗⠏⠀ ⠀⠪⡪⡪⣪⢪⢺⢸⢢⢓⢆⢤⢀⠀⠀⠀⠀⠈⢊⢞⡾⣿⡯⣏⢮⠷⠁⠀⠀ ⠀⠀⠀⠈⠊⠆⡃⠕⢕⢇⢇⢇⢇⢇⢏⢎⢎⢆⢄⠀⢑⣽⣿⢝⠲⠉⠀⠀⠀⠀ ⠀⠀⠀⠀⠀⡿⠂⠠⠀⡇⢇⠕⢈⣀⠀⠁⠡⠣⡣⡫⣂⣿⠯⢪⠰⠂⠀⠀⠀⠀ ⠀⠀⠀⠀⡦⡙⡂⢀⢤⢣⠣⡈⣾⡃⠠⠄⠀⡄⢱⣌⣶⢏⢊⠂⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⢝⡲⣜⡮⡏⢎⢌⢂⠙⠢⠐⢀⢘⢵⣽⣿⡿⠁⠁⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠨⣺⡺⡕⡕⡱⡑⡆⡕⡅⡕⡜⡼⢽⡻⠏⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⣼⣳⣫⣾⣵⣗⡵⡱⡡⢣⢑⢕⢜⢕⡝⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⣴⣿⣾⣿⣿⣿⡿⡽⡑⢌⠪⡢⡣⣣⡟⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⡟⡾⣿⢿⢿⢵⣽⣾⣼⣘⢸⢸⣞⡟⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀ ⠀⠀⠀⠀⠁⠇⠡⠩⡫⢿⣝⡻⡮⣒⢽⠋⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀

As someone who loves working with ASTs, it's great to know that that your viewers are interested in the topic! I loved the part where you implemented pattern matching, I had no idea how one would do that.

I really missed your content. You are my favorite KZfaqr atm. I hope that Putin will end his stupid war asap...

The functionality of this language is very reminiscent of the Wolfram language (Mathematica). It's described as 'term rewriting' or something like that. Thanks for sharing.

This is really neat. I've always wanted a system where I could input a math expression and "explore" the possible ways to manipulate it. Although in my case the idea is that the program would be able to visually show you different ways to manipulate the expression based off of all the various algebraic manipulations without needing them to be manually supplied the way your system works.

At 53:30, regarding capturing values, you can do so with a "move closure", as it's referred to within the Rust book.

We need a nice long rust-roast video. And what you think is better.

You r living in russia and u r putting a donation link for victims of war in ur description? i think this is a pretty brave act

this video is a gold mine for someone who would want to make a "tsoding out of context" vid

Damn, your topics are an incredibly interesting man. Cheers!

Thank you for all this excellent content

I love your coq replacement, thinking about replacing mine too

Great to have Tsoding back on YT!

Nice. I was working on something similar in swift. With an enum ast and SwiftUI rendering. I'm trying to practice calculus while creating the transformation

Very nice! What do you think of Isabelle/HOL?

Yay another vod!

I’ve considered doing something a little similar, except instead of having like, a general purpose AST, it just has tensor products and compositions? So, in the idea I’m imagining, each thing could optionally have a domain and codomain, which would also be things, and for a given pair of things (maybe requiring that the two things have the same “level”?) there would be the ordered pair (/ tensor product) of those two things (and if those two things had a domain and codomain, the product would also have a domain and codomain, and its domain and codomain would be the products of the domains and codomains respectively of the two things it is a product of) and if the codomain of one thing is the domain of another thing, they can be composed, Except, I think probably people have already made the thing im thinking of? Or at least something similar. But I don’t understand how to use their tool. It is apparently supposed to model infinity categories? So I guess I was thinking of maybe making a broken but easier for me to understand version of what they did.

Publishing amazing content. Then making a bunch of jokes about bad documentation == "job security". I was already a big fan. Now, reappearing from ashes and making jokes about hiding from KGB (I hope both are not literal), with a link to donations to the victims of war - and all of that without making any money for himself. That's true altruism, people.

I would have NEVER expected somebody who primarily programs in C and in Haskell to dislike Rust. The closest thing to a low level Declarative language, so yeah, pretty much a middle ground between those two

what about Lean to exploit their Tactics to create structures of proof templates ?

i leaned most from tscoding's strearm that i learned in university in 5 years.

Спасибо за видео, очень вдохновил, когда прога заработала, получил удовольствие, будто сам написал. Сейчас как раз это изучаем на дискретной математике, если не секрет, что заканчивал?

You should try a calculator with CAS support (Computer Algebra System). Smth like HP Prime. Not much bureaucracy there over derivative simplifications.

What font are you using? It looks so good

18:14 holy jeez i thought you were gonna use js

You are a fucking genius, i want give money for this amazing

Doesn't Prolog do this exact thing?

Hi. Really enjoying your channel for years. Can I support you from Russia somehow? Boosty maybe?

Regarding subscription: eventually, after the war is over and sanctions lifted, the money will get where it's meant to go. Otherwise, Twitch would be committing massive fraud by accepting the subscriptions.

not sure if you aware of this but i not get notifitcations of your videos anymore , I am in europe- the netherlands

51:10 never do "use some_module::SomeLongEnumName::*" as this can cause a bunch of issues down the line when you remove a variant, try "use some_module::SomeLongEnumName as SomeEnum" instead 👍

Why does it make you sad if someone uses emacs because of you. Looking how fast it works voor you it looks very nice. I wish I could use the keyboard as good and fast as you. That's harder in other IDE's than emacs I guess. Or do you have another opinion/idea?

YEP Coq

Nice T-shirt.

Nice

OCaml might be better instead of Rust, Coq is built with it.

Hello hello ❤❤❤

A new tsoding video. Made my day today. First viewer too.

5:53 bruv

😂 ya when CS students get board, they create functions and amusing mathworks projects.

Ofc you don't need money cuz the system you're making can automate and standardise the concept of a "process". This is the shit

i clicked because i am a rust shill

hehe... coq

How's going in Russia?

ладно

Am I the only one that h4t3s rust? I'd love to see you do this in pure C. That would be impressive, and more fun.

What Is your IQ??

A new tsoding video. Made my day today. First viewer too.