Microsoft Office has over 1.5 billion users worldwide

ем... вони включали в статистику всі інсталяції віндовс 11 де при кліку на *.XLS вискакує «Ексел» й каже «фігвам, заплати бабла»?...

Ну от рідна компанія мені зараз видала ноут з віндою, й там саме таке неподобство, то це вже мене порахували як юзера «Microsoft Office» чи ні?

Copilot

що сам собою з’являється з апдейтами (разом з рекламою на логін скріні) — теж багато хто не запрошував...
та й юзати його можна нахаляву з бравзера навіть зпід Лінухів))

PS/

Fortune 500 companies

моя теща точно працівник «Fortune 500 companies» тому їй дуже той «Офіс» та «Копілот» був би дуже потрібен :D
А я такий негідник не поставив «Офіса», від тещі «приховав правду»!

Авіація, NASA я думаю так. А там де я працював... Ок, припустимо драйвер відеокарти підвисне. Чи роутер перезавантажиться. Так, неприємно, але... 100% надійності не треба.

Ем... тобто всі побудови довкола авіації, то не «інсайди», а скорше «припущення»?

Тому Сішка, мова скоріше про зручність.

Тут, все ж, «вкусовщина», яку ще треба придумати як «міряти об’єктивно», зокрема й про те, за які аспекти зручності мова...

cmake на валідувати не треба, бо йому треба лише раз запустити збірку, у продакшені він не буде. Тобто це рівень A.

ем... напевно знову плутанина з буквами, бо «А» — самий легкий рівень «у нашій галузі», а «у вашій галузі» згідно цитати вище «Рівень A (Catastrophic)»...

Щодо валідації, знову ж таки, напевно залежно від галузі... «у нас» згідно постанов всі тули мають бути валідовані, й навіть вказуються в формальних доках що вносяться в спецільану систему й там трейситься що за домопогою чого створюється...

А от забули додати твердження про швидкодію, чи ліміти пам’яті, от це реальна проблема, бо formal verification доводить тільки те, що явно сформулювали в специфікації.

От я якраз про те, я не ставлю під сумнів тулу логічного виводу (хоча її також «у нас» провалідувати буде треба), а про те, що чєловєкі або нето пропишуть в реках, або ж не покриють все (я щось сумніваюся, що кожен доступ до масиву за індексом прописується окремо)...

... й, все ж, бракує «популярного викладу»... книжка по «веріфаєбл С» якось «не пішла»... магія з аналізом важкодобутого AST в екзотичній мові (що сама написана на екзотичній мові) — «нето», бо видається, що заставити HR знайти відповідних спеціалістів, або ж якось натрейнити їх — фантастика. Це треба щоб політехи/універи готували (там мало який випускник пригадує що таке Lisp, навіть на тих спецільностях, де його «вчать»), коротше задачка на роки й Rust з його популярними туторіалами вже ніразу не виглядає «оверкомплікейтед» порівнянно з навігаціюєю по AST й прувленням, що воно не зробить free двічі, також й в контексті того, що така навігація не скасовує інших активностей))

Ну тобто навіть коли я «здолаю поріг входження» й навіть переконаю начальство що C+Coq (чи + Rocq Prover, це ж так тепер звесться) буде точно ефективніше, ніж С + «оте все що я згадав вище», все одно «не взлетить» з вищеописаних причин

Ми плавно приходимо до «щоб теща не натисла „скачати сильна молитва за любого зятя.ехе“» достатньо їй поставити Лінух...
Й теща навіть не помітить різниці в своїх звичних «воркфловах» з бравзером...

Ну а за молодь, то як розповідати про небезпеки куріння, «мету», «фену», сексу без презіка і тому подібне, на то є завжди віра «то все для невдах, а от зі мною це не станеться» і тд...

верифікатора?

ну так, верифікатор верифікаторів верифікаторів для верифікаторів)) Коротше й тут чєловєкі не зникають, все одно хтось мусить до того дивитися

Саме так,
наразі ми встановили: бравзер, ігри,
от я хочу побачити відсоточок для «щось ще», таке, що окрім бравзера та ігр
(свій юзкейс з ВСКодом я закрив)

що ще?
для чого ще середня родина «простих сметрних» може поюзати комп, окрім
«бравзер» + «ігри»

наприклад: (піратські) музичка/фільми оффлайн... ну для цього кейсу ж теж Вінда не треба,
що ще, давайте накидаємо... ну?

(тут з за плеча підказують «піратський офіс»... хм... а що ним ще хтось користується? хтось взагалі «офісом» замість гугдоків користується? Великий відсоток тих кому умовний «Опен Офіс» не прокатить й саме в якусь обдаровану фічу «ворда» вперлося?)

але не професійних корнер кейс тулів за бабло, типу фотошопа, який «прості смертні» беруть з піратських помийок, а щось реально потрібне?

бо ж виходить, що вінда в наших краях стійка якраз завдяки ігри + щось з піратських помийок... але стоп, навіть тут я не можу придмати, що б я хотів зараз «нахаляву» на додачу до вищеперечисленого... ну але може справді, то я один «такий скромний»,
ну то давайте складемо список незамінних потреб массового користувача, до яких я, можливо/очевидно не належу :)

То рівень E автоматично стає рівнем A, тому що збій створює загрозу життю, або може призвести до авіакатастрофи. Рівень E це зазвичай допоміжні скрипти, тощо. Makefile наприклад.

точно, я все переплутав, бо в «нас» навпаки, чим більша буква, тим «зліше» рівень, й інша кількість рівнів северіті, але зміст я зрозумів :)

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

Наприклад, в статті, VerificationofType Checking andErasure forCoq,in Coq автори формалізували й частково довели коректність ядра Coq (перевірку типів та ерацію) всередині самого Coq, але через теорему Ґеделя про неповноту повну самодоказову коректність неможливо досягти, тому частина метатеорії лишається як аксіоми.

я трохи не про ту «валідацію», нукові праці можуть писати багато що...

я про те, що умовній організації *** (контролюючий орган в галузі, без якого девайс, з яким можливо «serious injury or death» не піде до юзерів) треба доказати, що дядечка який рів’ювить код й складає формальний документ можна замінити на тулу Coq.

Оце «доказування» (валідація процесу) про що «автоматизоване Coq катить замість алалізу складеного живою людиною» воно вже відбулося у вашій галузі?
(не знаю, як поянити, тобто «у нас» просто наукова стаття з якогото сайту для огранізації *** не прокатить, навіть якщо в тій статті «все правильно»).

Але... код CoQ не виконується, це інструмент типу cmake, відпрацював та видав результат. Якщо припускати злодія розробника у середині, то в принципі в більшості проєктів він зможе закласти міну.

ем... знову, напевно, не вмію поянити... «ми» не можемо використовувати на проекті, в процесі розробки «невалідовані тули», тобто якщо тула «показує покриття зелененьким», то, отже тут тулу також треба «провалідувати» за певною процедурою... й всі CMake й gcc (чи Візуал Студію) також валідують за певною процедурою (то не означає «верифікації» всіх фішок компілятора, а саме офіційне встановлення на придатність до «інтендед юз»)

От власне довкола того й питання: умовно «ваш відповідник нашого контролюючого органу», він не потребує «валідації Coq» в сенсі вказаному вище? Наукової статті з якогото сайту достатньо щоб «покрити» той рікваєрмент для «самого злого класу» й більше не потребувати послуг дядечка, який дивиться код й складає формальний документ?

+ ще, як «заміряти покриття», чи ми справді закрити все прекондішенами й посткондішенами? Тобто мова не про «злодія розробника» а про те, що може наші теореми доводять взагалі «нето» й нетам де треба...
якщо я десь забув написати/неправильно написав кондішени до теореми, що ми «не виліземо за межі масиву», й взагалі забув поставити такий асерт в тому місці, то тула «знайде сама» що я того не зробив? Чи ми знову повернулися до того, що хтось тепер має ще верифікувати наші прекондішени/посткондішени й те все, й чи ми їх вліпили де треба?

збій створює пряму загрозу життю або може призвести до авіакатастрофи

очевидно, софт рубається на частини, й кожна з них повинна жити в окремому давайсі/адрес спейсі, так же?

бо якщо Рівень A (Catastrophic) живе в одному адрес спейсі з Рівень E (No Effect), то з рівня E ми завжди можемо покоцати байтик рівня A, це ж логічно...

Вірніше, отже, все що живе в одному адрес спейсі з чимось «E», воно, отже таж «E», все вірно?

обов’язкові формальна верифікація та математичний доказ коректності.

Й мова саме (й обов’язково) про «автоматизований» процес, а не про дядечка «рів’ювера», що оформлює свій аналіз формальною докою про те, що й як він верифікував, й ставить підпис?

То CoQ, отже, вже валідували, щоб замінити того дядечка?
Якщо так, то круть, тоді скидаю капелюха))

а то вже до теми «right to repair» й всіх тих штук про які вповідає Louis Rossmann, про то, що тільки не придумають, аби створити людям нових граблів й «обламати» бізнес отим «незалежними ремонтникам»...

саме так й дивлюся, бо мені (як простому сметрному) більше нічого й не треба))

можна подивитися навпаки: яка різниця в тому, що там буде тією операційкою, яка хоститиме бравзер?
або: яка різниця в тому, що там буде операційкою, яка хоститиме ще й VSCode? ))

(звісно, я свідомо ігнорую корнер кейси обдарованих тулів, але який насправді відсоток користувачів тих обдарованих тулів?...
ну так, є ще аргумент за ігри, але ж Proton, нє? Та й кількість затятих гравців не така вже й велика, як здається...)

Лежить окремо в пісочниці, нікому не заважає, гроші приносить.

ну срачі ж продовжуються, отже, комусь таки «заважає»...
якби все було «безперспективно» то й навіть не пробували б

По факту це окремий процесс, якщо брати VST, то ми переводимо текст програми в AST, далі в CoQ формулюємо властивості до проводимо доказ. І так, CoQ поверне помилку. У мене стаття тут в листі очікування про верифікацію.

Оце було б цікаво почитати.

Теж саме відноситься і до Rust. Якщо брати авіацію, там не реліз, а сертифікація, DO-178C. Вони просто запитають: так у вас рівень A, показуйте вашу верифікацію. Тому хочеш не хочеш — мусиш.

В авіації, напевно все навпаки з буковками... буковка A чи буковка С «сама страшна»?

Тим не менше ніколи не чув, щоб юзали CoQ навіть для «самої страшної буковки» на тих проектах, про які я чув... Натомість покриття юніт, інтеграційними тестами (з спеціальними тулами, за великі бабки, що міряють покриття, й все має бути зелененьке), код рів’ю, ріск асесменти й мітігейшени... а от щоб «математично доведи тою тулою» — нє такого нема ніде...

Це ж треба було б, перед тим як взагалі почати юзати CoQ, ще й валідувати сам весь отой «процес верифікації за домомогою CoQ» й довести, що він забезпечує «покриття», й «нічого не втіче», й щоб «злі контролюючі організації» то признали взамін... хм, а взамін чого з вищеперечисленого? здається нічого з того вони викинути не погодяться, все одно «хочеш не хочеш — мусиш» робити те все решта, ніякого полегшення...

...та й щось гугль на запит «DO-178C and CoQ» не видає нічого отрім лєвого «Cost of Quality»... Тобто не видно, щоб то було включено в офіційний процес...
Я припускаю, що окрема організація може завалідувати додатковий (до тих що є) процес, але поблажок щодо попередніх їм за то все одно не буде

Ada працює в сегменті, де безпека важливіше за швидкодію. Знову, тести приховують маленьку деталь: зміна вимог, рефакторінг.

Звичайно, ну так Rust же також дає безпеку, нє? Й швидкий, практично, на рівні з Сшкою (не «в рази», а така різниця якась зовсім несуттєва)...

Ну й так, безпека важливіше, але чомусь обирають й «голу Сшку» замість «найбезпечнішої Ada», й навіть без всякого «CoQ», зато з «псевдо ООП фреймвормаки на Cшці»... й то все валідують й успішно пропихають навіть в такі девайси, де можливо «serious injury or death»...

(я веду до того, що Rust би унеможливив всі баги з розряду «хто покоцав цей байтик?», та ще й за сміховинну плату, але натомість й далі Сшка та г@вноімітація для «ООП», спагетті поінтерів, каст на касті кастом поганяє, та решта «приколів»...)

Здається, що саме Google зараз найактивніше просуває Rust у Linux kernel. Що, звісно, не гарантує успіху: Google+ , Hangouts, Inbox, Stadia, Glass... теж колись вважалися перспективними.

Зате Go живе й квітне, й навіть огидну потворку «Дарт» змогли прилаштувати в Флаттері вже після того, як на початкову ідею «заміни ЖС Дартом»... «поклали болт»... а ТайпСкріпт — дитя M$ теж цілком собі квітне))

А ти взагалі працював з ядром Linux? Писав драйвера?

ми вже про це говорили в іншому чатіку — лінкед лісти, RCU... там же й інший добродій приводив приклади як то все (дуже й «недуже») вирішується в Rust... а я плювався на методи витягувається всієї структурки з лінкедліста за допомогою макросів ()... ну й так, макроси, прості слова, глобальні змінні, DKMS...
... але ж наразі Лінус ще не здався з Растом, отже знає щось більше від нас))

Так і запишемо, Airbus це шаражкіна контора.

Ну ті потужні кантори, що юзають qp фреймворк — ніразу не «шарашкіни»... але як той, хто працював й епізодично ще працює з тим «індастріал грейд», можу відповідально заявити «qp фреймворк в його Сшній інкарнації — г@вно» ))

___
Airbus отже Ada, тут важко сперечатися з потужним «благословенням» від «перевіряючих органів», з іншого боку все якось сумно з продуктивністю, причому щось якось аж «в рази» і навіть гірше за Go...

А в Linux широковживана універсальна ОС, де безпека завжди йде в компромісі зі зворотною сумісністю, продуктивністю і новими фічами.

то за тими ж таблицями benchmarksgame Rust майже на рівні з няшною Cшечкою, отож може прижитися з безпекою та продуктивністю))

Зовсім не очевидно, команди процесора описуються формально, тому все на основі можна описати формально.

Описуються, але ж «далі» теж треба всюди юзати, тобто «без того доведення має генерувати помилку на етапі компіляції» примусово, інакше всі «верифікаці», якщо вони не повні — то «фіговий листочок»...

Це користувачу вирішувати, чи треба йому верифікація чи не треба.

ну так от тут якраз й головні граблі, що «це заскладно доводити що тут free — правильно», «тиждень до релізу», «ліньки», ще щосьтотам...
Тобто якщо верифікація опційна, то її будуть пропускати...

Так само як «забивають» й на решту речей, про що я вже описував вище...

зі схильністю до парадигмувань — спершу в секцію парадигмування, потім в секцію раст суперпозиції :)

то вже якась *уйня й неконструктив, як й з тим «диском Ц» в сусідній темі))

Контенту для пошукових запитів ми нагенерили вже достатньо, а за «філософією» — в секцію філософії, за «прогнозами» про «ШІ» в секцію до «ванги» й в «битву екстрасенсів»))

все легше (а часто і зручніше) працювати

для цього треба ще специфікувати, що таке «легше», «зручніше»...
Комусь типи «незручні», а хтось навпаки в динамічній мові «тайп анотейшени» ліпить...
Хтось хоче спочатку реки (чи спочатку тести), а хтось навпаки, спочатку код... Є лоюди що коментарів пишуть (й в тих коментарях їхні «шпаргалки»)), є що не пишуть, бо ліньки, не вміють (а «зпід палки» виходить «капітанщина», щось юзлесс таке що на от*бить), а є такі, що не пишуть принципово «бо так сказав дядко Боб» (тому часом моя перша їм порада — спалити книжку Стіва Роберта Мартіна, віддати в село бабі на підпалку))

(десь тут можна було б згадати астоср@чі про механіка vs автомат, але це «нете»...)

...дуже важко вже стало відслідковувати якість коду, тому треба просувати у себе в першу чергу, та щоб було де набирати людей з відповідними знаннями....

звичайно, вся проблема в тому, що знайти людину здатну вслідкувати за тою оверкомплікейтед кашою — все важче...
Та й навіть ті, що могли вслідкувати рік тому — вже не стягують))

то не люди «отупіли», то два фактори одночасно
1. Все ускладнилося «до ручки».
2. Відсоток населення, що органічно здатні братися за такі задачі й вирішувати їх якісно (навіть за велике бабло) — обмежений...

Ну.. по-перше навіть на Haskell писали операційну системи, більше як дослідження того, які проблеми виникають при цьому в чистих функціональних мовах.

Ну так, ось зараз поекспериментують з Rust, відшліфують, тай «щось буде», не дарма ж корпорації вкладають бабла... й то не одна якась а всі разом...

По-друге, особисто я не вірю в перспективи Rust в embedded, обмежень більше ніж користі.

Наразі звучить як «вкусовщина», бо для мене «примусовий RAII» виглядає навпаки «фічею», такий собі «лоу хенгінг фрут» щоб позбутися задачки «хто покоцав цей байтик в обдарованому сценарії?»

Ну... мінус швидкодія. Знову, ми про embedded та спінлоки? І знову ж, це не гарантія, що їх немає. Це означає, що їх не піймали.

Які спінлоки? Чому «мінус швидкодія»? Вочдог не повинен ранитися «весь час», й не повинен прівентити дедлок, він має його задетектити постфактум... звісно, 100% гарантії нема, але навіть бага «на філді» інвестігується, й легко знаходиться руткоз.

Це раз, є верифікатори. Тобто математичний доказ, що програма працює правильно, виконує специфікацію, не містить UB. Цим Rust краще? Зайві обмеження.

наразі виглідає так, що цим бавиться тільки «академія», й час «великої ідеї» не настав...
Rust краще якраз тим, що корпорації саме тут й побачили «велику ідею» й вкладаються баблом, тобто буде все готовеньке... ну й ті «обмеження» багато людей вважає «фічами», от так само, як й система типів, це ж «обмеження», ну але катить як корисна фішка навіть в Пайтоні тайпанотації, й лише для того, щоб ІДЕшечка підсвітила (не лише, їх в Пайтоні можна витягувати в рантаймі й робити цікаві речі))

Так, наприклад є формально перевірений компілятор Сі, правда більша частина на OCalm.

Тобто все ще дослідницікі проекти, що їх не просуває «жодна велика кантора»

Можна формалізувати інструкції процесора, можна формалізувати стандарт Сі (простіше ніж Rust), можна довести, до код, який буде згенерований компілятором формально відповідає стандарту.

А далі люди повинні засісти й написати рули для ядра Linux?
Чи переписати все по новій, щоб вкластися в те, що підтримує «формально перевірений компілятор Сі, правда більша частина на OCalm»?

Є, наприклад, веріфікований менеджер памʼяті з доказом того, що про alloc буде виділений новий фрагмент, а при free він буде звільнений, або буде помилка (до речі зроблений з аналогом FAT, тобто службова інформація про блоки міститься в іншому фрагменті памʼяті, тому якщо ми виходимо за межі, то ми просто залазимо на наступний блок даних, але не торкажмо службові дані.

Ем... ну так його ж й далі треба буде юзати з тими рулами й їх треба буде писати й далі, за межами менеджера памʼяті...

й, очевидно, що всюди будь яка операція, що «не підкріплена математикою», де не доведено, що вона «математично сейф й відповідає настановам», без того доведення має генерувати помилку на етапі компіляції, нє?

бо якщо писання прекондішенів, поскондішенів та решти «математики» — опційне,
то яка би крута не була реалізація malloc та free але завжди можна буде натупити з данглінг поінтерами й юз афте фрі чи меморі ліками і тд, якщо не примушувати користувача «довести математикою», що він має право ту free зробити саме отут... а ще всюди треба примусово щоразу довести що він не виліз за межі виділеної пам’яті, й не обов’язково послідовним записом, а й «яким попало»...

Оверкомплікейшен підтримки та розробки з раст?

Оверкомплікейшен всього проекту... згадувана make_u32_from_two_u16 то чиста Сшечка))
Просто саме на Rust дуже дуже акцентують увагу... воно звучить по новому...

А «maintainer burnout» помножене на «токсичність» Лінуса (та й решти мейнтейнерів) — відома річ...

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

Який там відсоток внесків від людей що працюють на корпорації, й отримують за те зарплату від корпорацій?
То може не так все й просто й райдужно з «найкращою системою в світі»... та й зробити форк, й послати «корпорації» разом з растом може хто завгодно, втім не дуже видно охочих...

Наймовірніше буде якийсь свій заморожений раст з bigtech поставкою розробників

саме так, саме так, воно сформується в щось більш стабільне, й саме за бабло корпорацій.

в іншому випадку завдяки відсутності стандартизації та занадто сподівань/надій на мовні засоби замість відлагодженої workflow з тестуванням

та не «замість» а «на додачу»)) ну й так, меморі баги, вони аж занадто анноїнг... хто покоцав цю структурку? трюк з датабрейкпоінтом робе тільки якщо бага репродюситься, проїходити всі оті стадії, переважно за чужою «творчістю» навіть для того, хто «вміє» — нецікавий й нетворчий процес...

Він не доводить логіку, він просто гарантує, що не буде помилок при роботі з памʼяттю. Що більш менш буде гарантувати люба мова з GC.

нє нє, не можна GC, ми ж в «ембедді»... треба щоб всюди «детермінований час» тому ніякого зависання на GC

Так, в багатопоточних застосунках гарантій трохи більше, але навіть гарантій вітсутності deadlock немає.

Звісно, але на деяких проектах, де мютекси/локи/івенти/черги/потоки з іменами, дедлок взагалі не проблема, адже вочдогом ловиться в рантаймі одразу, ще при тестах, й навіть пишеться в трейси хто й з чим напартачив (навіть якщо то рідкісний кейс, що репродюситься тільки «раз на мільйон» в продакшені, то з девайсу можна ті «трейси» добути й заінвестігувати що там нетак)

от як довести в Rust що програма не містить багів?

ніяк, але полюбе Rust — це вже краще за «голу Сшку» (навіть якщо на ту голу Сшку натравлено купу лінтерів, деяких навіть за великі гроші)

та й що значить «не містить багів»? для того потрібні реки/дизайн, бо «баги» то не лише умовний дедлок, а й відповідність «хотілкам» замовника, та ще й формально оформленим, щоб було відносно чого верифікувати (чого, насправді ніколи на 100% не буває навіть на «серйозних проектах»)

А на Сі з допомогою засобів верифікації я можу це зробити.

так, я пам’ятаю в мене десь навіть закладка десь є, на спеціальну обмежену версію С й тулу до неї, придуману якимись ученими, й дивний їхній сайт в стилі початку 2000х...

Але ж на умовному «нашому проекті» того (саме отої математичної тули) не юзають...
Взагалі ні на якому не юзають...
То виходить тула ще більш рідкісна ніж Ada...

Та ще й треба довести замовникам, що тула буде краще за ті валідовані лінтери, які вони юзають (звісно з джастіфікованими ексепшенами... інакше як би вийшло ту всю «кашу» замутити))

Ну тобто тула від вчених й спеціальна обмежена Сшка може й класні, але вони існують в якомусь «іншому світі», там, де не юзають (й навіть ніколи не чули) про «індастріал грейд qp» й всьо решта...

або зрозуміло з контексту

якого такого «контексту»? нема «контексту» на першому рівні, й на другому/третьому нема, бо воно лише в одній з опосередковано заюзаних АПІшок вилізло, й «обдарованому» сценарії... щоразу перебрати цей комбінароний вибух практично неможливо (нагадую мова про Cшку та структури даних з поінтерами й індірект викликами)

або клієнт працює з одного потока

Так, це була класна ідея: кожен об’єкт зі свого потока й оперує лише своїми даними, які йому передали у вигляді месіджів, в теорії це дуже круто, а на практиці руйнується одразу, якщо тільки в одній з тімів вирішили передавати чергами щось складніше ніж просто дані, й тоді геніальна ідея множиться на нуль.

Але... Подивися сирцевий код... Чи запитай LLM

таке працює тільки якщо обмежити рівні індірекшена, глибину вкладеності викликів, володіння об’єктами... тд...
коротше умовний Лінус повинен сидіти, й обкладати всіх матом, як тільки якийсь оверкомплікейшен!
А бо ж... ми знову «винаходимо» Rust...

PS. якщо що, то в кейсі «Лінус vs г@внофункція make_u32_from_two_u16» я, звісно, на боці Лінуса по всіх пунктах))

тоді то все ще сумніше...