Open artimath opened 3 months ago
the chicken isn't hatched yet! :)
btw you're probably the biggest direct influence into me suddenly deciding to spec out a new dependently typed lang, despite me having approximately zero expertise in language/compiler/interpreter design...
For now.
(I fantasize about formalizing all of undergrad math from the base type theory... All the LLM's tell me it's a multi-year journey for a team of mega-phd's...
Idk, I feel like if I define the problem properly, and have the appropriate tools on hand... We should be able to let a swarm of agents tackle it concurrently and shorten that considerably.
As long as the proof checker and type system are provably rigourius & valid.
Many humbling lessons ahead of me I would bet! 😂)
Anyway, thank you! Maybe I should start a textbook repo and record my entire learning process as I chip away.
I'd read that book haha
christmas came in july!!!