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

The software industry today is characterized by complex systems, such as parallel and distributed programs. These systems consist of a finite number of computational units that execute concurrently and synchronize with each other through message-passing, shared memory, or both, featuring increasingly integrated components and sophisticated functionalities. The scale and complexity of such systems are growing rapidly, and the pace of development has never been faster. However, this progress comes at a cost. With larger and more complex software, issues like unreliability, vulnerabilities, and unintended behaviors also increase. Ensuring the safety and correctness of parallel and distributed systems is as important as adding new features.

Formal methods are one of the prominent techniques that can provide theoretical guarantees and empirical tools to tackle these problems. In fact, formal methods offer formal specification languages that enable us to precisely model the behavior of each concurrent computational unit in a system, as well as the safety properties that need to be satisfied. Moreover, they provide sound, complete, and optimal decision procedures that allow us to perform automated reasoning over the formal specifications. Overall, they offer a push-button rigorous formal framework that can be applied to verify such systems.

In this introductory talk, we will motivate the audience regarding the need for formal methods in the daily software industry, followed by a discussion of some classical techniques that fall under the concept of model checking, which is an automated reasoning technique for verifying software. We will cover stateful enumeration, symbolic, and stateless techniques in model checking over guarded command languages, finite-state automata, and temporal logic formalisms. Finally, we will discuss state-of-the-art techniques in formal verification frameworks for concurrent and distributed programs and conclude the session with some open problems.

یکی از سوالای مفهومی کوبر اینکه وقتی یه دیپلویمنت اپلای میکنی چه اتفاقی میوفته تا اون پاد ایجاد بشه و قابل دسترس باشه
https://github.com/jamiehannaford/what-happens-when-k8s

چرا abstraction اشتباه در کد، از کد تکراری بدتر است:
https://sandimetz.com/blog/2016/1/20/the-wrong-abstraction

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

اگه جدولتون قراره سنگین بشه هر چیزی که توی ORDER BY می‌نویسید حتما براش Index بسازید ممکنه به مرور اپلیکیشنتون با رشدش کند بشه و نفمید از کجاست !


@Linuxor

ایده استفاده از لیزر ضد‌ماهواره #استارلینک توسط چین در مقالات آکادمیک و نظامی مطرح شده و در سطح پژوهشی مورد بررسی قرار می‌گیره، اما تا این لحظه مدرکی برای اثبات وجود چنین سیستم عملیاتی‌ای به‌طور علنی منتشر نشده ...
البته چین تنها کشوری نیست که نگران استارلینکه!

🔍 ircf.space
@ircfspace

گزارش کوتاه از وضعیت بازار کار مهندسی نرم‌افزار در سال 2025 که با Relocation همراه بوده است :
بیش از ۱۵۰۰ آگهی شغلی بررسی شده‌اند که از دارای (Relocation) بوده اند
- آلمان در صدر کشورهای منتشرکننده آگهی برای مهندسان نرم‌افزار بوده است.
- صنعت فین‌تک (Fintech) پرتقاضاترین حوزه بوده ، حتی جلوتر از حوزه های پر سر و صدای مرتبط با هوش مصنوعی.
- شرکت‌های متوسط و Scale-upها بیش از غول‌های فناوری (مثل MAANG) در حال جذب نیرو بوده و هستند

توزیع سمت ها و موقعیتهای کاری :
- برنامه نویسان بک‌اند ( که سلام و درود خدا بر آنها باد ): ۵۱۷ موقعیت (بیشترین تعداد)
- نقش‌های مرتبط با Data و هوش مصنوعی: ۳۵۲ موقعیت شامل: Data Engineer، Data Scientist، Machine Learning Engineer
- موارد مرتبط با DevOps و زیرساخت: رتبه سوم از نظر تقاضا

نتیجه: به شعور خواننده بستگی دارد !. ( البته به ما چه ؟! )

@DevTwitter | <Ali Kolahdoozan/>

https://chat.z.ai

من بجای claude ازش استفاده می‌کنم؛ البته کنار Qwen3-coder

اگر هم به طور خاص دنبال معنی کلمه‌ی خاصی از این اثر بودید بگید بهم :)

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

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

نام این اثر "پرچین" هستش.

ویس کال شروع شد ✔️