دیروز با یکی از دوستان سیستم کار داشتم صحبت می‌کردم و ۲ تا سوال داشت. یکی اینکه : مثلا الان اگه یک سیستم کانکارنت با چندین دیتابیس و کانکشن های مختلف همزمان روی یک ترد داشته باشیم ( مورد واقعی ) چطور میتونیم وریفایش کنیم؟ از کجا باید شروع کنیم؟ چیزی هست که فرآیند رو سریع کنه یا باید از ابتدا برناممون رو مدل سازی کنیم؟ دوم اینکه : یا راه درستی که میشه استفاده کرد اینه که از همون ابتدا verified توسعه بدیم برناممون رو؟

جوابی که من بهش دادم رو برای شما هم قرار میدم:

ببین جواب هر دو سوالت رو با هم میدم. اول از همه تو میتونی برنامه رو طوری توسعه بدی که از همون اول verified باشه، منتهی با هر زبان برنامه‌نویسی نمیشه این کار رو کرد. برای همین ممکنه خیلی جاها دستمون بسته باشه مثلا شرکت میگه که تو باید با زبان Go این سرویس‌ها رو بنویسی و خب ما هیچ فریمورکی نداریم که بتونیم به واسطه‌اش کد Go رو طوری تولید کنیم که verified شده باشه. منتهی خب اگر دست آدم باز باشه و بخواد یه سیستمی رو پیاده کنه بهتره که verified شده انجامش بده مثل همین پروژه‌هایی که بچه‌های MIT انجام میدن. چندتا مثال برات می‌نویسم:

DeepSpec / Sel4 / CompCert / Ironclad / IronFleet / CertiKOS / Formula-V / SCION / Barrelfish OS / ...

با چه زبان‌هایی این کارا رو میکنن:
Dafny - Boogie - Why3 - Coq - Isabelle/HOL - F* - Verus - Idris - Agda - Raven - SPARK - ...

اما خب همه‌ی سیستم‌ها که با این زبان‌ها نوشته نشدن و ممکنه ما یه سیستم مثل اونی که تو گفتی داشته باشیم و بخوایم وریفایش کنیم. چند تا کار میشه کرد. یکیش اینه که اون کد رو مثلا transpile کنی به یکی از زبان‌ها بالا. یکی دیگه‌اش اینه که سعی کنی رفتار برنامه‌ات رو مدل کنی. این کار رو باید با استفاده از زبان‌های فرمال انجام بدی و میتونی از هر یک از ابزارهای زیر استفاده کنی
TLA+ / Ivy / P / CIVL / JKind / SPIN
نکته اینه که اگر مدل سازی کنی، میتونی باگ‌های دیزاین و پروتکلی و الگوریتمی سیستم رو در بیاری. ولی چون خود کد رو verify نمی‌کنی ممکنه که کدت هنوز باگ داشته باشه.

برای وریفای کردن کد اومدن کلی تکنیک و و ابزار توسعه دادن. مثلا JMC که من روش کار میکنم برای وریفای کردن Java است. برخی از این ابزارها مبتنی بر روش‌های کلاسیک verification توسعه یافتن مثل symbolic model checking و Abstract Interpretation و CEGAR.

از بین این روش‌های کلاسیک میشه به اینا اشاره کرد :
CBMC (C) / JBMC (Java) / EBMC (Verilog) / Kani (Rust) / Viper (multi-lang) / CPAChecker (‌C) / Ultimate (C) / JayHorn (Java) / Farma-C (C) / Java Pathfinder (Java) / CN (C) / Nagini (Python) / Prusti (Rust) / BRiCk (C++) / coq-of-rust (Rust) / VerCors (multi-lang) / Verify Rust std lib / Verifast (multi-lang) / DSCheck (OCaml) / Rumur (C) / TriCera (C) / Eldarica (multi-lang) / Stateright (Rust)

منتهی نکته‌ای که وجود داره اینه که اکثر این ابزارها بخاطر محدودیت‌ها و سختی‌هایی که تصمیم پذیری روش‌های کلاسیک دارن، در مواجهه با کیس‌های real-world کم میارن. روش نوینی که برای verification کدها امروزه نشون داده که بسیار promising هستش stateless model checking نام داره که سعی کردم توی این پست توضیحش بدم. در این پست‌ هم لیست smc های موجود برای زبان‌های مختلف رو به همراه توانایی‌ها و محدودیت‌هاشون آوردم.

وقتی می‌خواین یک دادهٔ حساس مثل گذرواژه یا یک سیکرتی رو برای همکارتون بفرستین، معمولاً سریع‌ترین راه فرستادنش توی ایمیل یا ابزارهای پیام‌رسان مثل اسلک و تلگرامه. اما همون‌طور که می‌دونید این‌ها امن نیستن و بهتره پس از استفاده حذف بشن. با این حال خیلی وقت‌ها این اتفاق نمی‌افته. یا فراموش می‌کنیم، یا بدتر اینکه از همون پیام به‌عنوان پسوردمنیجر استفاده می‌کنیم!

یک راه‌حل ساده و در بسیاری از موارد، امن‌تر استفاده از ابزار 1ty.me هستش. این سرویس یک لینک حاوی اطلاعات مورد نظر براتون تولید می‌کنه و شما به‌جای خود داده، لینک حاوی اون داده رو می‌فرستین. خوبی‌ش اینه که لینک یک‌بارمصرفه و بعد از باز شدن، داده حذف می‌شه و دیگه قابل استفاده نیست.

@aminrbg

اگر روی مک هستین و از ollama استفاده میکنین یه سرویس مشابهش اومده که بیسش روی MLX هست و پرفورمنس بهتری داره

https://github.com/dinoki-ai/osaurus

@DevTwitter | <Armin/>

امروز شیرینی خورش (قاتق) پختیم ( یکی از غذاهای بسیار خوشمزه گیلان ) درست مزه شیرینی خورش های مامان بزرگ و مامانم رو میداد 😭

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

زبان برنامه نویسی PHP با کلی فریمورک محبوب و کاربردی...
زبان PHP که اولین نسخه اش سال ۱۹۹۵ منتشر شد، تا الان چندین فریمورک رو عرضه کرده که هر کدوم در زمینه های مختلف کارایی دارند.
از این فریمورک ها می تونیم لاراول، سیمفونی، کد ایگنایتِر، Zend و غیره رو مثال بزنیم.
در حال حاضر محبوب ترین فریمورک این زبان لاراول هست که اولین نسخه اش ۱۴ سال پیش (2011) منتشر شد و هدف از ساختنش ارائه جایگزینی برای فریمورک کد ایگنایتر و رفع محدودیت هاش بود.
این فریمورک هم فوق العاده قویه و هم بازار کار بسیار فعال و گسترده ای داره.
در حال حاضر بعد از لاراول فریمورک های سیمفونی و کد ایگنایتر محبوب هستن.
توی تصویر زیر به صورت خلاصه و جمع و جور آمار استفاده از فریمورک ها به همراه کاربرد سه تا از محبوب ترین هاشون رو آوردم.

@DevTwitter | <Parsa Kavian/>

مولانا | دیوان شمس | رباعیات | رباعی شمارهٔ ۴۸۹

آن کس که بر آتش جهانم بنهاد
صد گونه زبانه بر زبانم بنهاد
چون شش جهتم شعله آتش بگرفت
آه کردم و دست بر دهانم بنهاد

#مولانا | گنجور
📍@iipoem

یکی از بچه‌ها پرسید که آیا مکس پلانک تو زمینه‌ی ریاضیات هم موسسه داره؟ببینید ماکس پلانک یک انجمن هستش که متشکل از ۹۰ و خرده‌ای موسسه در زمینه‌های علوم پایه و علوم انسانی عه. در علوم پایه کلی موسسه در حوزه‌های ریاضی، فیزیک، شیمی و بیولوژی داره. به‌طور مثال در حوزه ریاضیات دو تا موسسه داره با نام‌های Max Planck Institute for Mathematics در شهر بن و Max Planck Institute for Mathematics in the Sciences در شهر Leipzig.
اگر دوست دارید ببینید که انجمن ماکس پلانک تو رشته‌ی شما چه موسساتی داره میتونید لیست موسسات رو از اینجا چک کنید :
https://www.mpg.de/institutes?tab=institutes

مثلا همین موسسه‌ی MPI توی شهر Bonn پروگرام دکتری داره و ددلاینش ۱۵ نوامبره. این لینکش. اونی هم که توی Leipzig هستش ددلاینش ۱ نوامبره. لینکش اینجاست.

آره خلاصه
هر روز مهمونی بود تو این مملکت
جشن دو هزار و پونصد ساله
هی توهین توهین توهین

چرا protobuf بد است و توسط یکسری جونیور طراحی شده؟!
نگارنده این مطلب خودش توی گوگل کار کرده و نظراتش رو در مورد اشکالات protobuf میگه مخصوصا تایپ سیستمش و این که مشکلاتی رو حل می‌کنه که به جز گوگل در جای دیگر وجود ندارن. حتی به عقیده اون، توی خود گوگل هم می‌شد کارهای بهتری کرد.
https://reasonablypolymorphic.com/blog/protos-are-wrong/

تبلیغ یه سایتی رو دیدم به اسم کیلوکد. جایی که می‌تونید با کمک هوش مصنویی، کیلویی کد بزنید😂

kilocode.ai


@Linuxor ~ mohsen1299

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

🔶 هر چه بیشتر جاوا اسکریپت یاد بگیری، بیشتر متوجه می‌شی که هیچ چیزی نمی‌دونی.

#توییت

@TheRaymondDev

یک سرویسِ email alias کاملاً رایگان از کشورِ لیتوانی که به تعدادِ نامحدود ایمیلِ مستعار می‌ده. تو هر سایتی با یک ایمیلِ مستعارِ جدید ثبت‌نام می‌کنید که به ایمیلِ اصلیِ شما فوروارد می‌شه. هروقت دیدید اسپم می‌فرسته ایمیلِ مستعار رو حذف می‌کنید و تمام.
https://yey.email

@DevTwitter | <Ayub/>

🔶 با شرط if در CSS به شما امکان می دهد سبک های شرطی را به صورت درون خطی بنویسید.

#css

@TheRaymondDev