day card at 29:00 (5am)

حسین خیلی خوبه، نازه، نرده. کم توقع هم هست. 100 امتیاز برای حسین.

چند وقت پیش با مشیا نشسته بودیم و داشتیم درباره اینکه علاقه ما چی بود و تهش برای گذران زندگی چطور مسیر کاری و دانشجویی ما توی این مملکت خراب‌شده تغییر کرد صحبت می‌کردیم. اون شب مشیا صحبت رو برد سمت فرمال متد و فرمال وریفیکیشن و گفت که توی کارهای R&D که انجام می‌ده از Lean4 استفاده می‌کنه و بهم پیشنهاد کرد که نصبش کنم و امتحانش کنم. باید بگم که واقعا قوی بود و ازش خوشم اومد. اگر نمی‌دونین این ابزارها چیکار می‌کنن باید بگم که خیلی کارها و واقعا نمیشه کوتاه توضیح داد ولی خیلی ساده اینکه بهتون کمک می‌کنن به صورت ریاضی اثبات کنین که سیستم نرم‌افزاری‌ای که نوشتین، کامل و درست کار می‌کنه و خارج از انتظار عمل نمی‌کنه. یک نقل‌قول معروف از دایسترا هست که می‌گه Program testing can be used to show the presence of bugs, but never to show their absence یعنی شما با تست کردن معمولی نمی‌تونین با قطعیت بگین که هیچ باگی در آینده در این سیستم وجود نخواهد داشت اما یک تضمین ریاضیاتی می‌تونه این کار رو انجام بده. خود Formal Method و Formal Verification یکی از شاخه‌های اصلی علوم کامپیوتره و روش‌ها و مباحث زیادی داره که به اون‌ها کار ندارم می‌تونین خودتون برین بخونین. این پست برای اینه که اگر خواستین محض سرگرمی یا برای کارهای تحقیقاتی یا پروژه کاری از فرمال وریفیکیشن استفاده کنین به جای ROCQ از Lean4 استفاده کنین. ممنون از مشیا بابت معرفی چیزهای جالبی که بدرد می‌خورن. در حد کارشناسی علوم کامپیوتر توی ایران که فکر نکنم اصلا کسی اینقدر ریز بشه توی درس، اما اگر ارشد، دکترا یا خارج از ایران دارین CS می‌خونین، به جای ابزار همیشگی دانشگاه‌‌ها یعنی ROCQ می‌تونین Lean4 رو امتحان کنین.

بسه دیگه

خب خب خب، همینجوری داره زمان میگذره و مشیا چیزی نمی‌نویسه از اونجایی شروع شد که میخواستم چندتا ضریب رو پیدا کنم، بعدش رسید به bode plot و lti، بعدش مجبور شدم برم سراغ Laplace transform و اعداد مختلط، بعدش مجبور شدم برم سراغ Fourier transform و بعدش least squares و optimization و بعدش Nelder-Mead بعدش درگیر c و fixed-point operation ها شدم. بعدش دیدم دارم SCO openserver 5 رو تست میکنم و دارم qemu کانفیگ میکنم. و دیگه کلا یادم نموند راجب چی میخواستم بنویسم 🚶🏼🚶🏼

آدم یکم غیب میشه ملت همینجوری لفت میدن 💔

جدی چیشد که یک ماه غیبم زد؟

یک زمانی صاحبان قدرت برده داشتن. بعدا قدرت از زور بازو به دانش تغییر جهت داد. ولی دانشمند هارو نمیشد به بند کشید. پس اونها دانش رو به گند کشیدن و اسمش رو گذاشتن مهندسی و دانشمند رو به بند کشیدن و اسمش رو گذاشتن مهندس

پیر شدیم کیومرث.

There's 10 kind of people, who understand binary and who don't. #dad_jokes

C language is so easy void (* (* f [ ] ) () ) () Defines an array with unexpected size of pointers to functions that return pointers to functions that return void

بی هدف ۱ حسین توی این پست خیلی قشنگ راجب چالش های کار کردن روی پرداکت های بزرگ نوشته بود، وقتی خوندمش هم دیدم که خیلی واقعی و درسته و هم دلم خواست یک نامه سرگشاده راجب کار کردن روی پرداکت های کوچیک بنویسم. هرچی که توی پرداکت بزرگ مجبورین تصمیم های نفرات قبل رو تحمل کنین توی پروداکت های نوپا و کوچیک مجبورین تصمیم های لحظه ای آدم هایی که از تخصصتون چیزی نمیدونن رو تحمل کنین. اغلب قدرت تصمیم گیری بالاتری داردین ولی.... مسئولیت خیلی بیشتری هم دارین... توی شرکت بزرگ مسئول اسپرینت خودتونین با تسک های محدودش و فیچری که کسی میبینه یا نمی‌بینه. توی یک سیستم کوچیک مسئول ددلاین های بزگترین، مسئول تجربه کاربر، مسئول بازگشت سرمایه، مجبورین تصمیم هایی بگیرین که تخصصتون نیست، باید بابت تصمیم هایی هزینه بدین که شما نگرفتینشون و در نهایت به خودتون میاین و میبینین تصمیم هایی گرفتین که توی یک سازمان بزرگ بقیه رو بابتش محکوم میکردین و بعد به خودتون میاین و میبینین تازه وارد ها دورهم توی کافه تریا جمع شدن و دارن زیر لبی شمارو فحش میدن :) یادمه راجب این قضیه با مهدی زیاد صحبت میکردیم، اونم همیشه میگفت: آقااا سرو ته بیزینس همش همینه... توسعه تا وقتی برای دلته خوبه وقتی میاد تو بیزینس دیگه کاریش نمیشه کرد.

نسخه جدید نامبان منتشر شد. تغییرات این نسخه شامل: - اضافه شدن DoH و DoT - دیزاین جدید مبتنی بر Adwaita - ریفکتور هسته اعمال تغییرات با منطق قبلی لینک لینک لینک لینک

2 سال گذشت :)

https://t.me/FouXNotes/1102

آقای George E. P. Box هستن تخصصشون آمار و احتمال بوده. و روی quality control, time-series analysis و bayesian inference کار میکردن. این جمله رو هم به ایشون نسبت میدن.

یک جمله معروف دیگه هم هست که میگه: All models are wrong, Some are useful.

Every mathematical model of a physical system is WRONG.

Every mathematical model of a physical system is WRONG.

زمان گرفتم، نوشتن این دوتا پیام حدودا 2 ساعت ازم زمان گرفت، واقع بینانه اونقدر که فکر میکردم تهیه کردن این محتوا برام راحت نیست، تازه این تازه فقط PID بود و هنوز دستکم 4 تا پیام دیگه هم مونده، احتمالا زمانبندی رو یکمقداری تغییر میدم.

day card at 29:00 (5am) pinned «جدول مطالب: # درباره اینترنت ۱. پروتکل tpc/IP قسمت اول قسمت دوم قسمت سوم قسمت سه و نیم قسمت سه و نیم و نیم ۲. رمزنگاری و TLS ( تا ۱۵ مرداد ) ۳. سرتیفیکیت و CA ( تا ۱۵ شهریور ) # سیستم های کنترل ۱. تاریخچه کنترل و علوم پایه مقدمه سیستم های…»