Distributed systems are notoriously hard to get right (i.e., guaranteeing correctness) as the programmer needs to reason about numerous control paths resulting from the myriad interleaving of events (or messages or failures). Unsurprisingly, programmers can easily introduce subtle errors when designing these systems. Moreover, it is extremely difficult to test distributed systems, as most control paths remain untested, and serious bugs lie dormant for months or even years after deployment.

The P programming framework takes several steps towards addressing these challenges by providing a unified framework for modeling, specifying, implementing, testing, and verifying complex distributed systems.

https://p-org.github.io/P/whatisP/

P is currently being used extensively inside Amazon (AWS) for analysis of complex distributed systems. For example, Amazon S3 used P to formally reason about the core distributed protocols involved in its strong consistency launch. Teams across AWS are now using P for thinking and reasoning about their systems formally. P is also being used for programming safe robotics systems in Academia. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone.

https://youtu.be/FdXZXnkMDxs?si=iFqpl16ONKZuS4C0

https://www.youtube.com/watch?v=_agDeiWek8w

https://github.com/rust-lang/polonius

توضیح نسبتا واضحی میده که borrow checker ( و lifetimeها) چطوری کار می‌کنه(‍/ن) (البته موضوعش پیاده‌سازی جایگزینی (Polinius) برای borrow checker هست که برای همین اول مجبوره که ورژن فعلیش رو توضیح بده)

#Alternative_Rock
#Persian_Rock

@Back_To_The_Start
.

https://github.com/adamtuft/c-kernel
زیباست

Algorithms for Modern Hardware

This is an upcoming high performance computing book noscriptd “Algorithms for Modern Hardware” by Sergey Slotin.

Its intended audience is everyone from performance engineers and practical algorithm researchers to undergraduate computer science students who have just finished an advanced algorithms course and want to learn more practical ways to speed up a program than by going from O(nlog⁡n) to O(nlog⁡log⁡n).

Part I: Performance Engineering
The first part covers the basics of computer architecture and optimization of single-threaded algorithms.

It walks through the main CPU optimization topics such as caching, SIMD, and pipelining, and provides brief examples in C++, followed by large case studies where we usually achieve a significant speedup over some STL algorithm or data structure.

https://en.algorithmica.org/hpc/

بیاین با هم بریم به دنیای RKHSها
قسمت اول: ‌kernel trick

درسته شبیه ولاگ‌ها شروع کردم ولی این یه بلاگه اونم راجع به Reproducing Kernel Hilbert Sapceها. اگه با من تو سفر ساختن یه فضای هیلبرت از ابتدا پیش اومدید(قسمت ۱ و ۲) و قبلترش چرا اصن فضای هیلبرت مهمه که اینجا در موردش حرف زدم، پیش اومدید بریم امروز ببینیم این فضای هیلبرت از نوع reproducing kernel چی هست. اگر هم فایل‌های قبلی رو ندیدید، توصیه میکنم با این شروع کنید دنیا رو چه دیدی شاید شما هم مشتری شدید.

اولش بگم که من خودم یه مدتی هست که بخاطر کاری که میکنیم با این کلمه‌ها و مفاهیم زیاد سر و کار دارم ولی بخاطر یه سوتفاهم (خدا نگذره ازت خانوم luxburg) نمیتونستم تفاوت بین kernel و reproducing kernel و در نتیجه فضای هیلبرت عادی و RKHS رو بفهمم. خلاصه امروز نشستم از اول و از چندتا منبع همه چیز رو خوندم و برام روشن شد. البته بحثایی که با علی‌ک کرده بودیم هم راهگشا بود. ولی قبل از اینکه بریم ببینیم دو به دو فرق این اسامی بالا و همینطور ارتباطشون با هم چیه بذارید اول بگم که به چه دردی میخورن اصن؟

فک کنم تقریبا همه‌ی ما یه درس آزمایشگاه تو دانشگاه داشتیم که یه سری داده رو اندازه گرفتیم و خواستیم بهترین رابطه خطی بین اون دو تا متغییری که مشاهده کردیم رو پیدا کنیم. این کار یعنی همون linear regression یکی از پایه ای ترین روش هاست در آمار و یادگیری ماشین/آماری. این روش خیلی خوبه دیگه چون با کمک جبرخطی و یه ماشین حساب مهندسی یا اکسل ساده میشه حلش کرد و تازه میشه به راحتی فهمید که چرا این خط انتخاب شده و ... . حالا بد روزگار اونجاست که رابطه بین هر دو متغییری که ما تو آزمایشگاه مشاهده میکنیم که خطی نیست که بیایم یه خط بهش برازش بکنیم. پس نیاز به مدلهای پیچیده‌تر داریم مثلا میتونیم یه سهمی برازش کنیم یا مثلا یه چند جمله ای از درجه سه با بیشتر🧐. ولی
ازون طرف وقتی مدلمون رو پیچیده کنیم پیدا کردن ضرایب اون چندجمله ای که بهترین برازش رو برای داده ما داره هم سخت‌تر میشه. پس چیکار کنیم؟ اینجور موقع‌ها میگن فضاتو عوض کن. یعنی صرفا به جای این که بخوایم y(متغییر مدنظر) رو برحسب یه عدد (x) پیدا کنیم میایم یه بردار میسازیم متشکل [x, x^2] بعد حالا y رو براساس این بردار جدید پیدا میکنیم. پس الان نقاط ما تو دستگاه سه بعدی هستن که یه بعدش x عه یکی x^2 و اون یکی y. یعنی داریم دنبال یه صفحه، y=ax^2+bx+c(در اصل دنبال ضرایبش) میگردیم انگار که به بهترین نحو به داده ما برازش میشه ولی اگه برگردیم به همون مختصات دو بعدی y بر حسب x میبینیم که یه سهمی داریم حالا. درست شد؟

حالا دقیقا از همین روش‌ها در دنیای روزمره برای پیش‌بینی قیمت خونه و ...بر اساس داده های موجود میتونیم استفاده کنیم ولی سوال این جاست که کدوم درجه برای مدلسازی ما مناسب‌تره؟ چه میدونیم تا حالا برازش نکردیم که (به قول دوست اردبیلی‌مون). مگر اینکه دقیقا فرمول ریاضی بین متغییرها رو بهمون گفته باشن که در اغلب موارد این طوری نیست. ولی خب حالا جدا الان که دارید میخونید حدسی ندارید که بهتره مثلا از یه چندجمله‌ای درجه بالا استفاده کنیم یا پایین؟

آره آفرین درجه بالا در نظر میگیریم فوقش اینه که اون ضرایب درجه های بالا صفر در میاد دیگه. خب سوال بعدی رو اگه ناراحت نشی بپرسم بالا یعنی چقدر؟ ۱۰ الان بالاست یا ۱۰۰ یا هزار یا یک میلیارد؟

خب هر چی بیشتر بهتر اصن. بینهایت چی نظرته؟ اع وایسا تو گفته بودی هر جا به بینهایت رسیدی مکث کن. اولا که برحسب کوییز آخر وقتی درجه چند جمله‌ای بی نهایت بشه که دیگه چندجمله‌ای نیست. آفرین دقیقا و برای همین پس میتونیم هر تابعی که دلمون میخواد رو باهاش تخمین بزنیم. ولی وایسا دفعه قبلی که درجه ۲ انتخاب کردیم تو یه بردار تو تو فضای R^2 درنظر گرفتی الان درجه رو بی‌نهایت گرفتی یعنی باید تو یه فضایی با بعد بینهایت کار کنیم؟‌اره دیگه برای همین اسم این بلاگ هیلبرته.

یعنی تو داری که میگی که من بیام تو ماشین حسابم یا اکسل یه سری بردار به طول بینهایت نگه دارم بعد اینا رو تازه وارون و ضرب و اینا هم بکنم؟
نه بابا اینکه نمیشه که اصن. خب د همین پس چطوری؟‌
خب سوال خوبی پرسیدی. راستش اینجا یه تردستی هست که بهش میگن kernel trick. به طرز جالبی تو محاسبه های مدل خطی مثلا برای رگرسیون و همچنین SVM ما نیازی نداریم که خود بردارهای با طول بینهایت رو داشته باشیم و تنها ضرب داخلی بین دو تا بردار رو نیاز داریم که یه عدد میشه و خبر خوب اینه که با توجه به قضیه های ریاضی که در سال ۱۹۵۰ توسط Nachman Aronszajn که یه ریاضیدان لهستانی/آمریکایی پیدا شده بوده میدونیم که میشه این ضرب داخلی دو بردار در RKHSرو به صورت ریاضی پیدا کنیم. چطوریش رو تو متن بعدی توضیح میدم.

مرسی که خوندی سوالی/نظری داشتی تو کامنت بگو.

#blog
@SingularThinker

این لکچر از جرمی اویگاد از کامپیوتر ساینستیست های خوب زمانه رو واسه کسایی که میگن چطوری میشه منطق امروزی شبکه های عصبی رو با برخی زیر شاخه های منطق ریاضی پیوند داد، پیشنهاد میکنم.
لکچر در Santa Fe Institute برگزار شده که از پیشرو های فیلد علوم پیچیدگی شناخته میشه.
https://youtu.be/lE48QtO4xBQ?si=oKPww1R5AiwoNIpW

یکی از خصوصیات جذاب این اینستیوت در این هست که همواره شرکت کنندگان از طیف وسیعی از رشته ها هستن
ریاضیات، بیولوژی، کامپیوتر، علوم اعصاب و حتی فلاسفه!

https://github.com/amirkhaki/jupyter_notebook_rtl

اگه notebook‌ فارسی می‌نویسید، این ابزار احتمالا به دردتون بخوره

کاری که می‌کنه اینه که cellهایی که باید رو (مثلا markdown فارسی)، توی یه div قرار میده و یک cell با کد جاوااسکریپت هم به ته notebook اضافه می‌کنه که اینا رو با css راست‌چین کنه.
خروجیش رو میشه بدون نیاز به نصب اکستنشن خاصی استفاده کرد.