Panch

@drunk_cachallot @yuriy_guts Так є bazzite і cachy

@yuriy_guts я хочу так шоб одной кнопкой ставити (клікати Next next next)

Я вже недочекаюсь Steam Machine та можливий реліз SteamOS окремий щоб навіки забути цю колись геніальну ос яку довели до повного пиздецю

@speed_shit Ще одна лінка проєбалась freshcodeit.com/blog/why-elixi…

@speed_shit Підтверджуючи про Elixir - у Teo нещодавно був відос на цю тему, де в сурсах тести Tencent з різними мовами youtube.com/watch?v=iV1Ecf… і хтось ще в статтю окрему розжував dashbit.co/blog/why-elixi… Захотілось спробувати jido

you dont need skills recently i was reading about Thiele Machine, a fun twist on the Turing machine that adds something like a "soul" to computation. cool rabbit hole. but it got me thinking about something practical. all these skills, rules, specs we feed to LLMs to make them code better.. they dont actually fix the root problem. the root problem is that an LLM generates code that *looks* statistically correct. and when you give it tests, it will happily bend the tests to match whatever it produced. plans, specifications, detailed prompts, all of these are just more text where the model can hallucinate or lose the plot. more surface area for things to go sideways. so i started looking at formal verification. specifically TLA+ for writing specifications and Lean for proving them. heres why this is different from just "better prompting". Lean has a proof kernel. its a tiny deterministic checker that either accepts your proof or rejects it. there is no "close enough". no statistical guessing. the LLM literally cannot bullshit its way through a Lean proof, the kernel will just say no. same story with TLA+, the TLC model checker will exhaustively verify your invariants against all reachable states. you cant sweet talk a model checker. but heres the fun part. i tried generating tests from TLA+ specs *before* any business code exists. the LLM that writes tests never sees the implementation. then separately, the business code gets generated within the constraints of a Lean theorem. two completely isolated contexts. the test generator and the code generator know nothing about each other. this is not TDD. in TDD you write tests based on your *understanding* of what the code should do. here the tests come from a mathematical model of the system. they encode invariants and properties, not example inputs and expected outputs. a TDD test says "when i call f(2) i get 4". a TLA+ derived test says "for all reachable states, this property holds and this transition is valid". the coverage is fundamentally different because it comes from the *shape* of the system, not from a developers imagination about edge cases. so you get: formal proof that wont let the LLM drift from the goal + business tests written before code even started existing + complete isolation between test generation and code generation. the model cant game what it cant see. and then today i see this: mistral.ai/news/leanstral mistral just released Leanstral, an open source agent built specifically for Lean 4 formal verification. literally yesterday. my take: all these skills and spec files we write today, thats a transitional period. within the next year SOTA models will be smart enough and formal verification will become a native part of code agents. when that happens its basically like C rising above assembly. you still need to understand whats underneath but you operate on a completely different level. p.s. also think about erlang/otp. it waited so long for its moment and now its rising from the ashes. OTP was literally designed and prepared for this. it maps perfectly onto the modern ai agents world. i even built a few implementations myself, and then openai came with github.com/openai/symphony (elixir on BEAM) and other folks shipped jido.run/blog/jido-2-0-… and suddenly building my own felt pointless =(

@speed_shit Ага, як раз хотів приклад моду для лаби привести. Для Bluetooth є DTM, котрий використовується лабой для рулінням TX і іншим, щоб потім видавати папірці. Звісно, це можна і в окрему фірмварю класти, але з точки зору розробки приємніше все тримати в купі docs.nordicsemi.com/bundle/ncs-3.2…

@dmpanch Причому прошивка дрону однакова. А FCC хак давно існує і його продають за 30 євро. І судячи з знайденого в офіційному додатку точно колись була кнопка для дебагу. Але вони прибрали тіло методу.

Okay, this is getting interesting. Ghidra MCP and Claude Code dug through the DJI Fly app and figured out how to switch the drone into “FCC mode.” And the funniest part: at the end it just said, “It’s already 2 AM. Let’s continue tomorrow.”

@speed_shit Взагалі не розумію як вони заробляли з їх ціновою моделлю

AI підібрався зовсім з іншої сторони. Цікаво, я про таке не думав.

@APolux @HorsyNox Перша рота дітей імператора

@HorsyNox Новопидорск Дристов по Говну Старий пидор Кроснопидорск Пидорский говнород Пидорово

До речі, не бачив ніде згадки про те, яке погоняло у тієї підлодки (підчовенки? підчовняки? 🤔). Бо «Варшавянка» то ж клас типу, а має ж бути ще погоняло якесь пафосне типу «Адмірал Говнов»

@APolux Трудовік після того як піздюку в живіт вилітає металевий штуцер: «Ти дурак, тебе посадять» А потім ще продавав їх десь на ринку

5 клас, труди у зош на драмнбасі: хлопці проходять у двері з дірою від вилетівшого диску з точильного верстату, включають станок стд 120м і хуярять підсвічники Перелякані в інтернеті:

Взагалі не фанат пана фізика, але тут програв так шо сопля вилетіла

@sergeykovalenko kyivhistorymuseum.org.ua/uk/exhibition/…

@speed_shit Батя і суп

GPUs are melting... А потім я просто все це квантизую в INT8...

@petrovkostya123 На другій фотці 6 школа

Десь між корпусами CНУ ім. В. Даля. 14.03.2013

На першому курсі, назбиравши грошей купив собі камеру. Тому ось тред гарних і не дуже фотографій Луганська 2013/2014 років. Буду вдячний за поширення. Може хтось з луганчан впізнає рідні місця. 14.03.2013

@bookazoid_ Торгану телевізором

@bookazoid_ Дякую за кунтент, захотілось повернутись до уроків, останнім часом більше по друку горів FYI, гарна стаття про дизайн деталей для друку blog.rahix.de/design-for-3d-…

Продовжую тицяти фьюжин. Та оскільки в мене вже майже чорний пояс по фьюжину який я отримав на йотубі, вирішив навести порядок з ось цим. Це два мікроконтроллери ESP32, яки майнять біткоїн з шаленою швидкість 60 кілохешей у секунду, воткнуті у пенопласт. Тобто блок вони знайдуть швидше ніж у росії настане демократія. Тобто десь за 15 хвилин до теплової смерті всесвіту.

@drunk_cachallot @bookazoid_ youtube.com/watch?v=WEIpQH…

@bookazoid_ а які ютуб відомо по фужену гарні рекомендуєте?

@c10ned @IsksbsN Оплата - не єдиний кейс використання NFC. ECP дозволяє навіть з вимкненим телефоном відкривати двері - register.apple.com/resources/docs…

Я не знаю. У випадку айфонів мені це не зрозуміло, бо оплата карткою там не активується при розблокуванні телефону, а потребує додаткових дій. Це якісь службові повідомлення, не уявляю для чого, напевно є така необхідність. Мене більше зацікавило те, що вони доволі голосні в радіоефірі.

Цікаву річ випадково помітив. Коли будь хто розблоковує смартфон - він посилає в ефір сигнал на частоті NFC (13.56 MHz). Гуглпіксель це робить якщо його розблокувати. Айфон посилає якщо просто увімкнути екран заблокованого пристрою, а також ще один, коли екран гаситься сам по таймауту, чи вручну. Посидівши буквально 15 хвилин на частоті я побачив, як сусіди масово перевіряли айфони, коли приходили сповіщення про шахеди. Це чудово працює через стіни, бо частота дуже низька. Не знаю, нащо вам ця інформація.

@Neyasit_alt @kapitandna Це gpt4o

@dmpanch @kapitandna А де це можна таке зробити?

Для тих хто не знав, повторюю свою офіційну заяву: Вважаю це фото з Луганську 90х найкращим фото в історії людства.

@kapitandna Будемо в тренді

@onoma_manul @icewithgintonic en.wikipedia.org/wiki/The_wrong…

У меня не было таких проблем с дойчебаном какие я испытываю в Англии 120 км из Лондона в Бристоль? Мы сделаем reroute посреди маршрута и поедем не 1.5 часа, а почти 3. Поезд в Бирмингем в 13:00 на билетах есть, а в расписании нет? Ну садись на тот, что в 13:45

@reformovane_zsu @vsheredeha Майже сюжет фільму «Маяк»

@vsheredeha треба ще якось вставить що пили вони разом

моє хемінгвеєвське найкоротше сумне оповідання про армію звучало б: «Пʼяний начальник бʼє пʼяного солдата за те, що він пʼяний»