جدی حالا این پیام چرا پرایوت شیر گرفته؟ دارین پرونده مرونده ای چیزی درست میکنین برام؟

Every mathematical model of a physical system is WRONG.

این جمله رو گوشه کنار های کتاب های مهم مهندسی میتونین پیدا کنین.

شاید فکر کنین بیشتر شبیه یک شوخیه ولی در اصل یکجور روتین فکر کردنه.

مثلا در عمل وقتی می‌خوان از روی یک مدل ریاضی نتیجه گیری کنن به اندازه ۲۰ درصد ! بهش نویز میدن.

یا مثلا اثبات میکنن !! اگه تا ۱۵ درصد تجهیزات خلاف مدل عمل کنن، سیستم واگرا نمیشه.

! چندین بار این نویز رو با روش ها مختلف تولید میکنن و تست میگیرن.

!! اثبات کلمه سنگینیه،‌ و قشنگیش همینجاست که اشتباه بودن مدل کسی رو از قطعیت عقب نمیندازه.

یک جمله معروف دیگه هم هست که میگه:

All models are wrong,
Some are useful.

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

این جمله رو هم به ایشون نسبت میدن.

2 سال گذشت :)

نسخه جدید نامبان منتشر شد.

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

لینک لینک لینک لینک

بی هدف ۱

حسین توی این پست خیلی قشنگ راجب چالش های کار کردن روی پرداکت های بزرگ نوشته بود، وقتی خوندمش هم دیدم که خیلی واقعی و درسته و هم دلم خواست یک نامه سرگشاده راجب کار کردن روی پرداکت های کوچیک بنویسم.

هرچی که توی پرداکت بزرگ مجبورین تصمیم های نفرات قبل رو تحمل کنین توی پروداکت های نوپا و کوچیک مجبورین تصمیم های لحظه ای آدم هایی که از تخصصتون چیزی نمیدونن رو تحمل کنین.

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

یادمه راجب این قضیه با مهدی زیاد صحبت میکردیم، اونم همیشه میگفت:

آقااا سرو ته بیزینس همش همینه... توسعه تا وقتی برای دلته خوبه وقتی میاد تو بیزینس دیگه کاریش نمیشه کرد.

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

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

#dad_jokes

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

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

پس اونها دانش رو به گند کشیدن و اسمش رو گذاشتن مهندسی
و دانشمند رو به بند کشیدن و اسمش رو گذاشتن مهندس

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

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

خب خب خب، همینجوری داره زمان میگذره و مشیا چیزی نمی‌نویسه

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

بسه دیگه

چند وقت پیش با مشیا نشسته بودیم و داشتیم درباره اینکه علاقه ما چی بود و تهش برای گذران زندگی چطور مسیر کاری و دانشجویی ما توی این مملکت خراب‌شده تغییر کرد صحبت می‌کردیم. اون شب مشیا صحبت رو برد سمت فرمال متد و فرمال وریفیکیشن و گفت که توی کارهای 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 رو امتحان کنین.

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