Forward from: JR TwitGram 🥂
Menimcha dasturlash haqiqiy “engineering” hisoblanishi uchun zo’r type system bo’lishi shart.
Hozir ko’pchilik dasturlarda “tahminan ko’p holatlarda ishlasa kerak” degan darajaga olib chiqilsa bo’ldi. Buzilib qolsa osmon uzilib yerga tushmaydi ko’p holatlarda.
Lekin bu haqiqiy engineering emas.
Siz yashab turgan uyni ham shunday qursa nima deb o’ylaysiz? “Aka, yashab turavering. Hudo hohlasa yaxshi bo’ladi. Tahminan qo’ldan kelgacha qurdik. Lekin 100% garantiya bera olmaymiz.” desa?
Shuning uchun ham bu narsalar haqiqiy engineeringa asoslanadi. Haqiqiy engineeringda qurilgan narsa ishlashiga isbot bor.
Dasturlashda esa yo’q. Shuning uchun ham dasturlash hozircha haqiqiy engineering emas.
Bu tarafga endi sekin sekin yuryapti.
Automated reasoning, verification, prop testing degan narsalar bor. Ular yordamida yozilgan kodni ishlashiga qaysidir darajada “garantiya” bersa bo’ladi.
Amazondagi men ishlayotgan jamoa ham Automated Reasoning bilan shug’ullanadi. Biz yozgan Cedar tili masalan shu tushunchalardan foydalanib yozilgan. Yani uni ishlashiga matematik isbotlar mavjud.
AI rivojlangan sari ham bu narsalarning muhimligi oshib boradi. AI yozgan kodlarni isbotlash uchun.
Type System ham qaysidir manoda shu isbotlarning bir qismi. Compiler kodingiz ishlashiga type systemdan foydalanib garantiya bera oladi.
Hozir ko’pchilik dasturlarda “tahminan ko’p holatlarda ishlasa kerak” degan darajaga olib chiqilsa bo’ldi. Buzilib qolsa osmon uzilib yerga tushmaydi ko’p holatlarda.
Lekin bu haqiqiy engineering emas.
Siz yashab turgan uyni ham shunday qursa nima deb o’ylaysiz? “Aka, yashab turavering. Hudo hohlasa yaxshi bo’ladi. Tahminan qo’ldan kelgacha qurdik. Lekin 100% garantiya bera olmaymiz.” desa?
Shuning uchun ham bu narsalar haqiqiy engineeringa asoslanadi. Haqiqiy engineeringda qurilgan narsa ishlashiga isbot bor.
Dasturlashda esa yo’q. Shuning uchun ham dasturlash hozircha haqiqiy engineering emas.
Bu tarafga endi sekin sekin yuryapti.
Automated reasoning, verification, prop testing degan narsalar bor. Ular yordamida yozilgan kodni ishlashiga qaysidir darajada “garantiya” bersa bo’ladi.
Amazondagi men ishlayotgan jamoa ham Automated Reasoning bilan shug’ullanadi. Biz yozgan Cedar tili masalan shu tushunchalardan foydalanib yozilgan. Yani uni ishlashiga matematik isbotlar mavjud.
AI rivojlangan sari ham bu narsalarning muhimligi oshib boradi. AI yozgan kodlarni isbotlash uchun.
Type System ham qaysidir manoda shu isbotlarning bir qismi. Compiler kodingiz ishlashiga type systemdan foydalanib garantiya bera oladi.