"Beware of bugs in the above code; I have only proved it correct, not tried it."
به نظرم همین طعنه‌ی آقای Donald Knuth میتونه لازم و کافی باشه جهت ساپورت کردن این نکته که روش‌های Formal Verification که Statefull هستند (به قولی semantics-driven) و یا مبتنی بر Static Analysis هستند (به قولی Syntax-driven) اصلا مناسب برنامه‌هایی که با یک real programming language نوشته میشن نیستن. بهترین راه، اجرا کردن برنامه است و روش‌های مبتنی بر اون مثل Stateless Model Checking چرا که اگر باگی در برنامه وجود داشته باشه قطعا در runtime بهش میرسیم. این جمله آخر رو دوبار بخون چون من راجع به testing و fuzzing صحبت نمی‌کنم.

از اصحاب کسی پرسید که Stateless Model Checking چیست؟ و ما برایتان پست‌هایی نوشتیم مثل:
"از زاربروکن تا کایزرسلاترن : Stateless Model Checking"
"Software Verification is Our Quest"
"Fuzzing for free! Except you, concurrency!"
و حتی این، تا برایتان پندی باشد. باشد که مطالب کانال را دنبال کنید :)

از اصحاب کسی پرسید که Stateless Model Checking چیست؟ و ما برایتان پست‌هایی نوشتیم مثل:
"از زاربروکن تا کایزرسلاترن : Stateless Model Checking"
"Software Verification is Our Quest"
"Software Verification is Our Business"
"Fuzzing for free! Except you, concurrency!"
و حتی این، تا برایتان پندی باشد. باشد که مطالب کانال را دنبال کنید :)

قرار هست یه تب جداگانه AI به واتساپ اضافه بشه در کنار ویجت AI تا دسترسی به Meta AI آسون‌تر بشه.
اینا توی یه نسخه آزمایشی اندروید یعنی ۲.۲۵.۱.۲۷ دیده شده و فعلا معلوم نیست کی به نسخه اصلی اضافه میشه.
نتیجه احتمالا اینه که Meta AI میتونه تو بازه زمانی کمی تعداد کاربران خودش رو به این روش میلیاردی کنه.
wabetainfo
@geekalerts

ادوبی سرویس Adobe Firefly Bulk Create رو معرفی کرده که میشه باهاش تا ۱۰ هزار عکس رو همزمان با AI ویرایش کرد.
کارهایی مثل تغییر سایز عکس‌ها یا تغییر پس زمینه و ... رو انجام میده.
احتمالا برای کسایی که حجم زیادی عکس برای ادیت دارن میتونه مفید باشه و خروجی انبوه بگیرن.
ادوبی یه سری API جدید هم برای Firefly Services معرفی کرده که به زودی در دسترس قرار می‌گیرن مثل دوبله و هم‌گام‌سازی لب‌ها یا آواتارهای دیجیتال و ...
https://firefly.adobe.com/
theverge
@geekalerts

چین داره بررسی میکنه اگه نتونن جلوی ممنوعیت تیک‌تاک‌رو توی آمریکا بگیرن در مورد فروشش صحبت کنن و حتی به گزینه‌هایی مثل ایلان ماسک فکر کردن.
البته ByteDance همیشه میگه هیچ ارتباطی با حکومت چین ندارن و معلوم نیست جلساتی که چین میذاره و داره تصمیم میگیره با اطلاع ByteDance هست یا بدون اطلاع اون‌ها.
میگن چین روی کار اومدن ترامپ رو یه چالش برای خودش میبینه و تصمیم داره با فروش تیک‌تاک به آمریکا درهای توافق رو با آمریکا باز کنه.
البته خیلی هم راهی نداره چون بخش بزرگ کاربرهای این برنامه توی غرب هستن و اگه آمریکا ممنوعش کنه به صورت دومینو تو بقیه کشورهای غربی هم ممنوع میشه.
ولی اصل این اتفاق نشون میده چین تصمیم داره دوران دوری از تنش رو دنبال کنه.
bloomberg
@geekalerts

🔶 گوگل در حال حذف حساب‌ و اپلیکیشن توسعه‌دهندگان ایرانی است؛ چون برای ما ایرانی‌ها، امکان احراز هویت وجود ندارد.

@TheRaymondDev

🔶 دوست عزیزمون دیاکو که افزونه کروم برای راست چین سازی چت دیپ سیک توسعه داده است و البته ممکن است که در آینده قابلیت راست چین زبان خاورمیانه ای (غرب آسیا) اضافه کند.

این افرونه مرورگر کروم بیس ها قابل نصب است.

گیت هاب :

https://github.com/diakohamidian/rtl-deep-seek

@TheRaymondDev | @Diako488

تلگرام مسابقه برای توسعه‌دهنده‌ها درست کرده و ۲۰۰ هزار دلار جایزه میده به شرکت‌کننده‌های برتر.
در کنار اینکه این فرصت رو دارن که به تیم تلگرام و TON ملحق بشن و یا کدشون برای بهبود بلاکچین TON استفاده بشه.
مهلت تا ۴ فوریه هست و تسکی که قراره انجام بشه اعتبارسنجی بلاکچین (بهینه‌سازی کد C++) و ... هست.
اطلاعات بیشتر رو توی کانال TON میتونید پیدا کنید.
@geekalerts

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


@Linuxor ~ Mosher's Law

نسخه بتای «تسک‌ها» (Tasks) توسط OpenAI راه‌اندازی شد.
این همون ویژگی هست که از ChatGPT میخواید یه سری چیزهارو بهتون یادآوری کنه و یه سری تسک براتون درست کنه.
مثلا بهش بگید جمعه‌ها بهتون بگه کتاب بخونید، یا هر روز اول صبح یه جمله انگیزشی بهتون بگه.
یا خرید‌های هفتگی و پروژه‌ای که باید تحویل بدید رو یاد آوری کنه.
یعنی کافیه با ChatGPT چت کنید و ازش بخواید تا اون لیست تسک‌ها و یادآوری‌هاتون رو خودش درست کنه.
این ویژگی میتونه بخش بزرگی از مردم دنیا که فرایند نوشتن تسک و کار کردن برنامه‌ها براشون سخته رو به برنامه‌ریزی و نوشتن تسک علاقه‌مند کنه.
الان برای کاربران پلاس هست ولی گفتن رایگان برای همه منتشر می‌کنیم.
x
@geekalerts

لوس آنجلس چرا شبیه گیم Doom شده

خیلیا سایت حتی حرفه ای و خفن می‌سازن و دلسرد می‌شن که چرا سایت ما نمی‌گیره؟

ساده ترین جوابی که می‌شه به این سوال داد اینه : سایت شما ارزش افزوده کمی داره، یعنی چیزی به کسی اضافه نمی‌کنه... یه سایت وردپرسی با ساده ترین دیزاین ولی یه خدمات مفید و بر طرف کننده نیاز، می‌تونه به راحتی از سایت شما با خفن ترین تکنولوژی بازدهی بیشتری داشته باشه.


@Linuxor

برنامه‌ی سریع با کوپایلوت

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

#javanoscript #html

Black Candy
سرور موزیک سلف هاست ، برای رهایی از تحریم های اسپاتیفای ، ساند کلود و از دست رفتن پلی لیست ها...
🔗 github.com/blackcandy-org/blackcandy
🆔 @Hiradsajde

Kasm Workspaces
با استفاده از این پروژه ، میتونید فضای کارتون رو روی مرورگر تون داشته باشید،
برای سرور های خارج دغدغه لایسنس ویندوز بابت ریموت دسکتاپ نداشته باشید،
از اینترنت پر سرعت دیتاسنتر ها همراه با آیپی ثابت و اتصال ایمن استفاده کنید!
🔗 kasmweb.com
🆔 @Hiradsajde

من با اینکه ادمین این کانال رو نمی‌شناسم ولی واقعا پیام بسیار حقی توی کانالش نوشته. متأسفانه این قضیه‌ی fake hype ای که کتگوری تئوری ایجاد کرد گریبان فرمال کارا رو هم گرفته به نوعی که توی کنفرانس‌های حوزه‌ی ما رو بگردی کلی پیپر پیدا میکنی با عنوان A Categorical Framework یا A Categorical foundations یا حتی مییرن سمت semantics و کلی A Categorical Semantics داریم :)) تهش هم واقعا پیپر رو میخونی میبینی که خیلی حرف خاصی وجود نداره و صرفا داره نون Category رو میخوره.

حتی کامیونیتی PL کارا هم به شدت مسوم شدن، هی راه می‌افتن دنبال مپ کردن Category و Functional که البته کار درستیه منتهی خب متأسفانه از مسیر درست خارج شده و بیشتر شبیه Show شده و صرفا جنبه‌ی show-off کردن و گنده خفن پنداری داره. مثلا طرف میاد میگه اگر Free Monoid نمیدونی چیه یعنی اصلا programming نمی‌دونی چیه. خلاصه این مقالات مسئله‌ای حل نمیکنه و صرفا ابزار خوبی شده برای تولید مقاله