Awesome

داشتم رندوم دنبال دوره کاتلین می‌گشتم توی یوتیوب و از ۶ تا دوره خوبی که پیدا کردم، ۵ تاشون استادش هندی بود. و به طرز جالبی ترجیحشون می‌دم چون انگلیسی اون‌ها نیتیو نیست و خیلی راحت‌تر می‌تونم تلفظ‌ها و صحبت کردنشون رو متوجه بشم. 😁

هر وقت خواستین به این فکر کنین که AI می‌تونه اثبات قضایای ریاضی رو راحت‌تر کنه یادتون باشه که قبل از اون Proof Assistant‌هایی مثل Lean4 و خیلی قبل‌تر از اون ROCQ توی این کار پیشرو بودن و ابزار خود AIها برای این کار هم همین‌هاست.

چند وقت پیش با مشیا نشسته بودیم و داشتیم درباره اینکه علاقه ما چی بود و تهش برای گذران زندگی چطور مسیر کاری و دانشجویی ما توی این مملکت خراب‌شده تغییر کرد صحبت می‌کردیم. اون شب مشیا صحبت رو برد سمت فرمال متد و فرمال وریفیکیشن و گفت که توی کارهای R&D که انجام…

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

دسکتاپ سینامون در عین سادگی اما یکی از بهترین تجربه‌هایی بوده که داشتم. شباهت زیاد به گنوم و کاستومایز به شدت راحتش باعث می‌شه بدون دردسر هر کاری رو به راحتی با چهار تا کلیک انجام بدین. یک مقداری بعضی چیزهایی که می‌خوام رو نداره ولی باز هم تجربه خیلی خوبی تا به الان بهم ارائه داده. خیلی قبل‌تر می‌خواستم یک سشن کلا سینامون داشته باشم ولی وقت نکرده بودم. یک مورد دیگه اینکه من خیلی Hot Corner استفاده نمی‌کردم ولی الان با سینامون و dpi بالای موس عملا هات کرنر نباشه فلج می‌شم. :)

Hallusquating نتیجه اخلاقی؟ هیچوقت به ایجنت‌ها دسترسی کامل ندیم یا اگر دسترسی کامل نیست و داره سوالی می‌پرسه همینطوری از سر بی‌حوصلگی اوکی ندیم.

از اونجایی که سشن Wayland Wayfire کلهم پرید و مجبور شدم برگردم به X11، گفتم چرا استایلش ویندوز ۹۵ نباشه؟ پ.ن: این تصویر قطعا جالب به نظر میاد ولی هیچ یکنواختی‌ای وجود نداره چون GTK و Qt و باقی چیزها اصلا بهم نمی‌خوره استایلشون و حوصله درست کردن همه چیز رو ندارم. جدای از اون اپ‌های الکترون و کلا همه چیز، استایل جدید دارن و لزوما استایل سیستمی ندارن که بتونم عوض کنم و حال و هوای رتروی تم رو خراب می‌کنن.

هیچوقت (همیشه) سعی نکنید (کنید) xfce رو بدون xfwm4 و روی wayland با wayfire بالا بیارین. فقط دردسره (شاهکاره)

https://blinry.org/multi-seat-wayland/

https://blinry.org/multi-seat-wayland/

عرفان عربی رو بردن حبس. :(

صفحه اول کانفیگ مرورگر Helium :)

واقعا گاهی اوقات به این فکر می‌کنم که SysAdmin ویندوز بودن چقدر آزاردهنده می‌تونه باشه. فکر کن مثلا روز کاری به ادیت کردن رجیستری یا اسکریپت نوشتن تو پاورشل بگذره. یا مثلا فرض کن بخوای تصمیم بگیری یک طوری Partial آپدیت یا حتی آپدیت کامل انجام بدی ولی یک بسته‌ای رو نخوای. یا فرض کن قدیم‌تر برای اتومیشن با ویژوال بیسیک می‌نوشتن. (پاورشل نبود اصلا) بعد من واقعا درکی ندارم ولی جعبه ابزارشون دقیقا چی داره توش؟ تا حالا سیس ادمین ویندوز از نزدیک دیدین؟

How Windows architecture looks like now:

بهترین Naming Convention وجود ندا... پ.ن: از مزایای همکار بودن با زکریا

این چنل یک چنل شت‌پست روسی بود که از خیلی وقت پیش توش بودم. داشتم پست‌هاش رو نگاه می‌کردم و این رو دیدم. جدای از اینکه این تصویر واقعی باشه یا نه، نمونه واقعی این رو یک بار توی ردیت دیدم. یک ویپ Hayati Pro بود فکر کنم که میکروکنترلر ۳۲ بیتی داشت که بر پایه یک سری خاص از آرم بود. این میکروکنترلر کامل قابل Re-flash بود و اومده بودن روش یک دونه RTOS (Real Time OS) بالا آورده بودن. واقعا بعید می‌دونم بشه روش کرنل بالا آورد. اگر دیدین برام بفرستین ببینیم.