Qiziq maqola ekan, Lean4 bilan salgina tanishganimdan kegin aynan amazon ham shundan ko'p foydalanishiga guvoh bo'lgan edim. Kegin
@keilambda TLA+ kabi narsalardan ham foydalanishini aytdi ))
Fikrimcha dasturlash sohasida aynan manashunaqa narsalarga extiyojlar ko'payabti. Chunki mavjud bo'lgan traditional yechimlar doyim ham o'zini oqlamayabti. Masalan mani tajribamda bir tizim uchun architecturedan tortib hamma narsani documented qilish va uni doyim update qilib yurish juda qimmatga tushgan edi. U yetmaganidak turli dunyo qarashdagilar turlicha tushunadi. Masalan requirements bo'yicha QA test qiladi ammo fichani bug deydi... Yoki yozilgan testlarda exeptionlar barbir chiqadi.
Prooflar bunaqa muammolarning davosi. Ammo ko'pchilik learning curve deb bunaqa narsalardan uzoq turadi. Lekin business uchun aynan manashunaqa yechimlar arzonroqga ham tushadi deb o'ylayman.
Masalan architectlar uchun TLA+, Alloy6 kabi toolar juda ham foydali instrument. Sababi siz qanaqadir diagramlar bilan emas balki aniq propositionlar bilan define qilasiz tizimni. Diagramlar sizga aniq muammoni ko'rsatmaydi siz shunchaki UML chizasiz. Ammo UML shunchaki rasm u bilan nimadirni isbotlash yoki tekshirish qiyin yani inson faktoriga asoslangan.
Ammo biz 21 asrdamiz, xozirda hamma narsa juda complex bo'lib ketgan. Barcha edge caselar inson miyyasiga sig'maydi. Shu sababdan bizga boshqacharoq narsa kerak. Bu narsalar bizni xato qilishdan saqlashi yoki xatoyimizni ko'rsatishi kerak. Fikrimcha bunaqa point of view bizga ancha qulayroq va effektivroq deb bilaman.
TLA+ at amazon:
https://awsmaniac.com/how-formal-methods-helped-aws-to-design-amazing-services/Lean4 at amazon:
https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math