گوشی و دستگاه‌های جولیا هم ضبط شده بود و نمیتونست به حساب‌هاش توی تلگرام و اینستاگرام دسترسی داشته باشه.
همین سکوت هم باعث شده شایعه وب‌لاگ‌نویس‌ها بیشتر بشه و جولیا مورد آزار و اذیت سایبری قرار بگیره.
جولیا قوی موند ولی برخلاف من به این روند‌ها عادت نداشت، دو روز پیش پیش دکتر بارداریش رفت و فهمیدیم که قلب بچمون دیگه نمیزنه.
https://t.iss.one/julivavilovaa/304
@geekalerts

هزار و یک باگ
شب دوم - قسمت اول
—————————————————

یک شب دیگه، یک برنامه‌ی دیگه و یک باگ دیگه. نمی‌دونم چرا ولی همیشه یک سری کارا خیلی ساده به نظر میان. مثلا فرد چندتا رمان روسی میخونه، موزیک‌های نئوکلاسیک فانک راک گوش میده، کمی تئوری لرنینگ میخونه، از SVM عبور می‌کنه و سعی میکنه ماهیت استوکستیک LLM ها رو درک کنه و بعدش به خودش میگه که من تونستم جفت پوچ بودن دستای هستی رو رو کنم، منتهی با گذر زمان میفهمه که انقدر هم اینکار ساده نیست و حتی نمیتونه یک random walk رو توجیه کنه. میفهمه که خیلی عقب وایساده و قرار نیست فیزیک و شیمی مدرن نظری جلوش زانو بزنن. مثلا شخص اثبات کرده که مسئله‌ی ارضاء پذیری ساختارهای محدود در منطق مرتبه‌ی اول، تصمیم ناپذیره، و فرد میگه که کی همچین زری زده :) من میرم براش یک الگوریتم P مینویسم، منتهی باید کلی روحش سوهان بخوره تا بفهمه راحت که هیچ، شدنی نیست.
این مقدمه شاید لازم بود تا برسیم به مسئله‌ی مورد بحث که بسیار ساده است. محاسبه‌ی ب.م.م دو عدد با روش اقلیدسی. اگر تا حالا اسم این الگوریتم رو نشنیدید اصلا چیز مهمی نیست. من بهتون توضیح میدم. تصور کنید که شما یک تابع دارید که دو عدد صحیح a و b رو به عنوان ورودی میگیره. این دو عدد بین دوتا Thread به اشتراک گذاشته میشن. ترد اول چنین کدی رو اجرا میکنه

Thread I
while ( a != b ) {
    if ( a > b ) {
        a := a - b
    }
}

ترد دوم هم به قرینه‌ی ترد اول همین کار رو تقلید میکنه. یعنی چنین کدی رو اجرا میکنه :

Thread II
while ( a != b ) {
    if ( b > a ) {
        b := b - a
    }
}

بیاید برای درک بهتر الگوریتم یک مثال رو اجرا کنیم. تصور کنید مقدار a و b به ترتیب 10 و 4 باشه. ترد اول بعد یک بار اجرا مقادیر جدید a و b رو به شکل 6 و 4 در میاره. توجه داشته باشید که در طول اجرا ترد دوم فقط میتونه به شکل idle در حلقه بمونه. سپس ترد اول یک بار دیگه اجرا میشه و مقادیر a و b به 2 و 4 تغییر میکنن. حالا ترد اول فقط میتونه به شکل idle لوپ بخوره و ترد دوم بدنه‌ی if رو اجرا کنه. پس از یک بار چرخش، ترد دوم مقادیر a و b رو به 2 و 2 تغییر میده. حالا هر دو تا ترد میتونن با یک بار اجرای حلقه، از while خارج بشن و حاصل ب.م.م. دو عدد هم همونطور که ملاحظه می‌کنید در a و b قرار داره که 2 می‌باشد.

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

fun foo() {
    int a = nondet()
    int b = nondet()
    assume ( a > 0 && b > 0 )
    
    a := a_in
    b := b_in

    ThreadI  ( a_in, b_in ) -> start
    ThreadII ( a_in, b_in ) -> start

    ThreadI  -> join
    ThreadII -> join

    int guessed_gcd = nondet()
    assume (  guessed_gcd > 1 )
    assume ( a_in % guessed_gcd == 0 )
    assume ( b_in % guessed_gcd == 0 )

    // Properties
    assert( a_in % a == 0 )
    assert( b_in % a == 0 )

    assert( a >= guessed_gcd )
}

حالا پرسش ساده‌ای که مطرح کردم و فرمال می‌کنم.

۱. آیا می‌تونید خودتون با استنتاج روی این کد اثبات کنید که برنامه این Properties رو ارضاء میکنه یا نه. اگر آره استنتاج‌تون رو شرح بدید.

۲. آیا می‌تونید یک برنامه‌ا‌ی بنویسید که به عنوان ورودی این برنامه رو از شما بگیره و اگر حالتی درش وجود داره که منجر به نقض شدن شرط‌های assert میشه رو پیدا کنه و به عنوان یک مثال نقض بهمون یک trace از اجرای برنامه برگردونه؟ اگر چنین برنامه‌ای نوشتید، آیا decision procedure که برای پیدا کردن این trace به کار بردید، sound و complete و optimal هست؟ لطفا اثبات کنید.

هزار و یک باگ
شب دوم - قسمت دوم
—————————————————

این بار می‌خوام برخلاف هزار و یک باگ‌های قبلی کمی مسئله‌ رو پیش ببرم تا نشون بدم یک مسئله‌ی به این سادگی تا چه اندازه میتونه پیچیده بشه. فرض کنید برای وریفای کردن این برنامه ما میتونیم متغیرهای a و b رو به شکل symbolic در نظر بگیریم. یعنی هیچ مقدار مشخص ندارن. حالا فرض کنید که ما یک oracle یا پیشگو داریم (در حقیقتا یک SMT Solver) که در هر لحظه از اجرای برنامه می‌تونیم بهش یک فرمول منطقی بدیم و ازش بپرسیم آیا این فرمول ارضاء پذیر هست یا نه. حال با داشتن این دو یاور شروع کنیم به درستی‌یابی برنامه. در ابتدای اجرا می‌دونیم که :

a > 0 && b > 0

به قول معروف، without loss of generality فرض کنید که ترد اول اجرا میشه و به اولین فرمول سیمبولیک بر میخوره یعنی a != b حالا نوبت استفاده از اوراکله. ازش می‌پرسیم آیا ممکنه این فرمول ارضاء پذیر باشه ؟

a > 0 && b > 0 && a != b

اوراکل میگه بله و مشکلی نیست برو جلو. فرمول بعدی a > b هستش و دوباره اوراکل رو صدا می‌کنیم :

a > 0 && b > 0 && a != b && a > b

اوراکل میگه بله اگر مقدار a برابر با b + 1 باشه این فرمول ها ارضا پذیرن. بعد از اجرای دستور a:= a-b و رسیدن به شروط حلقه و if دوباره باید اوراکل رو صدا بزنیم :

a > 0 && b > 0 && a != b && a > b && a-b ! = b && a-b > b

اوراکل میگه بله ارضاء پذیره. کافیه مقدار a برابر باشه با 2b+1. دوباره ترد یک ادامه میده و حلقه رو یک بار دیگه پیمایش میکنه و میرسیم به این پرسش از اوراکل :

a > 0 && b > 0 && a != b && a > b && a-b ! = b && a-b > b && a-2b != b && a-2b > b

اوراکل میگه بله ارضاء پذیره چرا که مقدار a میتونه برابر با 3b+1 باشه. بعد از n بار اجرای حلقه، پرسش از اوراکل میشه :

a > 0 && b > 0 && a != b && a > b && a-b ! = b && a-b > b && a-2b != b && a-2b > b && ... && a - nb != b && a - nb > b

و اوراکل میگه چون مقدار a میتونه برابر با :

(n+1) b + 1

باشه این فرمول ارضا پذیره. همونطور که ملاحظه می‌کنید پورسه‌ی وریفیکیشن یک برنامه‌ای که میشه اثبات کرد halt میکنه، تصمیم ناپذیر شده و تا بینهات ادامه میده و هیچ وقت converge نمی‌کنه! و یک مسئله‌ی به این سادگی اونقدرا هم که فکر میکنیم ساده حل نمیشه.

نسخه جدید چت‌بات مایکروسافت Copilot اومده و برای دسترسی بهش کافیه کشور رو روی آمریکا تنظیم کنید.
قبل از این کار باید به حساب خودتون لاگین کرده باشید.
https://copilot.microsoft.com
@geekalerts

بحث سافتور وریفیکیشن که گفتم توی این پست در مورد همین مطالبی هستش که توی پست‌های "هزار و یک باگ" بهشون می‌پردازیم. برای آشنایی با این فیلد میتونید ۳ پستی که با عنوان هزار و یک باگ گذاشتم رو بخونید.

در ضمن دلیل اینکه گفتم بهم پیام بدید و یکمم از خودتون بگید این بود که منم با شماها بتونم آشنا بشم و همه چیز صرفا unicast نباشه.

وقتی اینترنت نمیتونه مشکلت رو حل کنه 😂

#fun
@CodeModule

حق 👌
درواقع این همین <توهم بدن شناگر> هست. این باور جا افتاده که شناگر ها بدشون عالیه، چون شناگر هستن. درصورتی که این باور توهمه، و اگه کسی مثل شناگر ها ورزش کنه لزوما نمیتونه بدنش عالی باشه.
درواقع ریشه این مشکل اینجاست:
Correlation is not causation
که نمیتونم خوب ترجمش کنم

@PyBackendHub

یه منبع غنی آموزش دانشگاهی کامپیوتر از دانشگاه های هاروارد، پرینستون، MIT و ...

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

https://github.com/ossu/computer-science

🐧 @Linuxor

میخوایی بدونی پس قضیه جاواسکریپت چی میگذره و توی مصاحبه ها هم ازش استفاده کنی ؟

من یه مجموعه مقالاتی به اسم اندراحوالات جاواسکریپت توی سایت ویرگول نوشتم که جواب سوال بالا رو بهت میده:
تا جایی که تونستم هر موضوعی رو به ساده ترین نوع ممکن توضیح و پوشش دادم

اندر احوالات جاوا‌اسکریپت قسمت اول
در مورد نحوه کار js و javascript Engine
https://vrgl.ir/fH7sf

اندر احوالات جاوا‌اسکریپت قسمت دوم
در مورد Execution Context, Call Stack و زیر و بم اش
https://vrgl.ir/REWoF

اندر احوالات جاوا‌اسکریپت قسمت سوم
هر آنچه که باید درمورد Scope و مخلفاتش بدونی
https://vrgl.ir/Zr7QI

اندر احوالات جاوا‌اسکریپت قسمت چهارم
در مورد Hoisting
https://vrgl.ir/A3CVT

اندر احوالات جاوا‌اسکریپت قسمت پنجم (آخر)
در مورد مفهوم this و کاربردش، arrow function و bind
https://vrgl.ir/JpJXp

نبرد async و sync
در مورد مفهوم asynchronous و synchronous - میکروتسک چیه؟نحوه کار کرد؟
https://vrgl.ir/96eJP

@DevTwitter | <Mohammad Bohluli/>

🏰 اولین بازی استراتژی آنلاین در تلگرام! 🏰

قدرت در انتظار شماست...

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

شما، برترین پادشاه خواهید شد. 👑

🎮 @CastelGame_bot @CastelGame_bot
🎮 @CastelGame_bot @CastelGame_bot

اگه سردرد گیت داری و بعضی از مواقع اصلا نمیدونی چه کامندی از گیتو بزنی، این برنامه سبک یه GUI ترمینالی برای گیته


https://github.com/jesseduffield/lazygit


توصیه میکنم اینو توی خفا استفاده کنید به هیچ وجه کسی اطرافتون نبینه نصبش کردید.


🐧 @Linuxor

یادداشت های go

در تمام دنیا VPN ابزار افزایش امنیت کاربره؛ هرکی به‌غیر از این گفت بدونید یا نادانه، یا بر اساس منافع خاصی داره واقعیت رو وارونه جلوه میده!
کسی که به فکر امنیت کاربره نه پروتکل‌های امن رو مختل/مسدود میکنه، نه مارکت‌های امن و معتبر رو میبنده و نه سرویس‌ها رو ⁧ #ایران_اکسس⁩ میکنه.

© vahidfarid

🔍 ircf.space
@ircfspace‏⁧

📌جستجو متن دلخواه در درون محتوای فایلها و فهرست📌

🔸اگر شما یک توسعه‌دهنده، برنامه‌نویس وب، یا فردی هستید که با تعداد زیادی فایل کار می‌کند و به دنبال پیدا کردن یک قطعه متن هستید، یادگیری و به خاطر سپردن یک فرمان خاص برای شما سخت است. به عنوان مثال، فرض کنید یک دایرکتوری دارید که شامل 30 پوشه و 20,000 فایل است. مهم نیست که پسوند فایل‌ها چه باشد؛ آن‌ها می‌توانند .txt، .php، .css، .js و غیره باشند.
شما نیاز دارید که به سرعت یک متن یا چند کلمه را در این فایل‌ها پیدا کنید. چه کار باید بکنید؟ قطعاً بررسی هر فایل به صورت جداگانه غیرممکن است، بنابراین فرمان grep در لینوکس به کمک شما می‌آید.

فرمان grep یکی از قدرتمندترین و چندمنظوره‌ترین فرمان‌های لینوکس است. هدف اصلی آن جستجوی الگوها در هر فایل است و از قوانین پیچیده نیز پشتیبانی می‌کند.

grep -rnwi '/path' -e 'your_text'

🔸اگر گزینه w رو بگذارید دقیقا همان کلمه مدنظر برمیگردد مثلا cat
🔸اگر گزینه w رو نگذارید کلمه های دارای حروف cat باشند برمیگرداند.
🔸گزینه n شماره خطی که متن پیدا شده برمیگرداند.
🔸گزینه r هم درون فهرست های تودرتو جستجو انجام میدهد.
🔸گزینه i به معنی ignore که به بزرگ یاکوچک بودن حروف حساس نمیشود.

نویسنده: حسین سیلانی
منبع : کانال لینوکسی: لینوکس تی ان تی
@linuxtnt

حمایت از کانال-donate
https://zarinp.al/learninghive.ir