Yana ham soddaroq aytsak - qiymati emas qadri baland loyihalardan yaxshi startup chiqadi.

Qiymatni suniy ravishta oshirsa bo'ladi ammo qaripastligicha qolaverishi mumkin.

Masalan xozir har qanday AI agentdan oson vos kechishingiz mumkin. Kompaniyalar ham agar hohlasa bazi narsalardan oson vos kechishi mumkin. Birnecha bor qatnashganman A servis o'rniga B servisni integratsiyasida.

Lekin bazi yechimlar haqiqatdan takrorlanmas va ularning qadri baland. Shunchaki vos kecha olmaysiz.

Masalan Absint Lubis eda kompaniyalarini birinchi bor eshityabsiz ammo ularning mijoz yoki hamkorlari ro'yxatini qarasangiz hayratga tushasiz ))

Absint - Critical realtime tizimlarni formal verifikatsiya qilish uchun software ishlab chiqadi.

Lubis eda - Harware design digital systems verification related mavzuda model checkerlar va prooflar ustida ishlaydi.

Ha bunday kompaniyalar qilish uchun shu mavzularda shug'ullanadigan odamlarni to'plash kerak, bizda esa xozircha bunaqa odamlar yo'q desa ham bo'ladi. Fikrimcha markaziy osiyoda ham bundaylar juda kam bo'lsa kerak.

Qizig'i ham shunda, xozirda progressiv rivojlanayotgan paytimizda bunday mavzularga yetib borishimiz imkoni baland. Ammo ishni boshlash uchun kerakli hechnima yo'q, venture fondlar bu mavzularni tog'ri baholab pul ajratmasligi ham mumkin. Lekin long termda qarasangiz umuman tesha tegmagan bozor, researchni o'zingiz boshlaysiz, ochiq maqolalardan o'rganib nimadirlar sinab ko'rsangiz bo'ladi. Hohlasangiz aynan bir mavzuda PHD topib keginchalik tezisni startupga aylantirasiz. Lekin shuncha sayi harakatga arziydi agar yaxshi mavzu topilsa. Bozor yo'q degani paydo bo'lmaydi degani emas, talabni siz paydo qilishingiz mumkin. Agar tor sohalarda bo'lsangiz shundoq ham hamma uchun qilmayabsiz yechimni bu esa o'ziga yarasha katta imkoniyat degani.

Masalan formal methods related researchalar ham juda ko'p sohalarga integatsiya qilingan. Ayniqsa xozirda talab juda oshib boryabti, masalan Lean4 degan tilni LLM bilan integatsiya qilib LLMlar bergan outputlarni tekshirishyabti. O'ylaymanki yana boshqa juda ko'p mavzular huddi shunaqa. Ha bular ancha niche sohalar va katta mexnat talab etadi. Lekin natijasi arziydi chunki qadri baland qiymati suniy ravishta oshirilishi qiyinroq.

Leaked data ichida manam bormanmi deyman 🥲

Cooked endi chetdan call bo’lmaydi

Hullas banklar leak bo’lmasa bo’lgani hammasi nazorat ostida.

AGAR supportga yozib 2FA o’chirishmasa.


Steamda ham skinlarim qolmagan mobodoga.

zoomrada investment bo'limi ochilgan ekan kirib aylanib yurib down qilib qo'ydim.

Kechirilar 😢

Shuni invest qilmoqchi edim ahir.

yana qanaqa investment platformlar bor load test qilib beraman ?

10 soat mazza qilganmiz, meetupga borib bunchalik mazza qilganimni eslolmayman.

O'ziyam juda qiziq bo'ldi.

4 soatda compiler yozdik va 1.5 soat parsing combinatorlar bilan tanishdik yani parsing uchun bir texnikani o'rgandik kegin GHC generics bilan boilerplate codeni kamaytirish haqida gaplashdik.

Essentials of Compilation mavzusini ko'rishni hammaga tavsiya etaman.

Lean4: How the theorem prover works and why it's the new competitive edge in AI

https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in

Theorem proverlar g'oyasi kechagina paydo bo'lib qolgan narsa emas.

Man bilganim Automath project eng birinchi teorem proverlardan batafsil: https://automath.win.tue.nl/

Umuman olganda bu mavzular asosida juda ko'plab ishlar qilib kelinyabti. Theorem proverlar katta tarixga ega bo'lsada haligacha juda aktiv izlanishlar qilib kelinyotgan sohalardan.

Umuman olganda bu sohalar ham raqamli dunyoning bir ustuni desak bo'ladi. Mavzular atrofida juda ham ko'p qiziq tadqiqotlar mavjud. Hozirgacha SAT solverlar o'rtasida raqobat bor, kim tez ishlaydigan SAT solver qilishga musobaqalashadi: https://satcompetition.github.io/

muhim bo'lgan deyarli hamma crashlar yeg'ilyabti endi :)

bunisi surpriz bo'ldi macosda

Hullas 3ta devaysim xozir actual.

1. PC - Ram ECC bo'lmaganiga memory corruptionlar handle qilinmaydi.
2. Laptop Nixos - HDMI ishlamaydi hamma narsa qilib ko'rganman faqat Type-C bilan monitor ulay olaman baxtimga.
3. Macos - Kayfiyati yaxshi bo'lasa ishlaydi.

Bu narsalar shunchalik kulgiliki - man umrimda biror muammosiz laptop yoki telefon ishlatib ko'rmaganman.

Oldingi devayslarimda ham muammolar bor edi. Manimcha yangilarida ham muammolar chiqadi.

Manam video qilsamikan.

One day of my life deb.

ORB stack nixos machineda ishlata oldim vanihoyat.

Macos uchun parallels ishlatmasdan ham nix yengil nix machine run qilsa bo'lar ekan.

Load deyarli sezilmaydi albatta build paytida ko'proq ram yeyabti ammo bu chepuxa muhimi build bo'lyabti.

Hullas ORB stackda unstable nixos run qivordim va baxtliman.

Tez orada configimni ham ulashib qo'yaman.

Conflict-free Replicated Data Type (CRDT)

Introduction: https://mattweidner.com/2023/09/26/crdt-survey-1.html

More resources: https://crdt.tech/resources