لماذا يصنع أبناء الأرض برامج وأجهزة عربات التي تجرها الدواب

, - . , , — , ..

, , , , , , «» , - ( ExoMars).

.

1. — , , . , , . , - , , , .
   
   
2. / / — , , . , , 160 , .
   
   
3. / — . - «, », « », « ».

, .
, , homo sapiens « » , - , .

, , , , .

, « ?», « ?», « ?», « ?» .

, — . , Zcash CryptDB, , , , .

من أجل القول - "نعم ، يعمل البرنامج على النحو المطلوب" ، يجب أن يكون لديك دليل رياضي على هذا البيان ، للأسف لست خبيرًا في هذا المجال ، ولكن بقدر ما أعرف أن عملية هذا الإثبات معقدة للغاية ، ولكن لا ينبغي أن يكون هذا عقبة للأسباب التالية:

1. لا توجد طريقة أخرى ، أصبحت أنظمتنا أكثر تعقيدًا ، وتعتمد طبقات جديدة على القديمة ، ولكن للأسف هذا ليس أساسًا موثوقًا به للغاية.
   
   
2. تحتاج إلى إثبات البرامج الصغيرة ( Unix Way ).
   
   
3. من الضروري فقط إثبات البرامج المهمة لموثوقية الموثوقية. لا يمكنك إثبات صحة مجموعة المكتب ، ولكن يجب إثبات نواة نظام التشغيل أو مكتبة التشفير.
   
   
4. , , - , , , , .
   
   
5. (Haskell?). , - , .
   
   
6. , .

بالطبع ، لا يخلصنا إثبات البرامج من الحاجة إلى صياغة المتطلبات بدقة ، ولكن أعتقد أن هذه مشكلة قابلة للحل ، خاصة أنه في بعض الحالات (مثل مكتبات التشفير) يتم إضفاء الطابع الرسمي على المتطلبات نفسها.

أعتقد أن الجميع يرغبون في برامج موثوقة تمامًا للعمل في محطات الطاقة النووية ، في المعدات الطبية وأماكن مماثلة.

لن أقول أنه كان من الضروري القيام بذلك لفترة طويلة ، حيث كانت الصناعة تتطور بسرعة ، وقد تغيرت الكثير من الأشياء بشكل كبير ، ولكن اليوم ، من وجهة نظري ، الصناعة ناضجة بما يكفي لبدء ترتيب الأشياء.

هناك فئات جديدة من المهام مثل أجهزة الكمبيوتر الكمومية والمعالجات المتخصصة للشبكات العصبية ، كل شيء بدأ للتو. لكن تطوير هذه الصناعات لا يلغي الحاجة إلى نهج كلاسيكي - كل شيء له مهامه الخاصة.

تعتمد الحضارة الأرضية الآن بشكل كبير على موثوقية أنظمة الكمبيوتر ، ولكي لا تتراجع في الليل عن ضوضاء أجنحة نقار الخشب الطائر ، يجب أن نبحث عن حلول تزيد من الموثوقية.


بشكل منفصل ، تجدر الإشارة إلى الشبكات العصبية ، الشبكات العصبية هي محاولة لنسخ الدماغ بكل إيجابياته وسلبياته ، الحل على الشبكات العصبية يحتوي على نفس المشاكل مثل الدماغ البشري ، لذلك يجب تطبيقها فقط حيث لا نعرف كيفية حل المشكلة باستخدام الرسمي الخوارزمية تعمل بشكل موثوق للغاية.

أعتقد أنه من أجل أن تتطور الحضارة الأرضية بشكل مطرد ، فقد حان الوقت للتفكير في موثوقية بنيتها التحتية ، فيما يتعلق بتكنولوجيا المعلومات التي أراها بهذه الطريقة - تحتاج إلى تحديد / إنشاء لغة برمجة رياضية عالية المستوى والبدء في إنشاءها بالكامل (بدون الملفات المخفية تحت غطاء المحرك) البرامج الأكثر أهمية مع دليلهم اللاحق. من المحتمل أن يتم إثبات وصياغة بنية الأجهزة للمعالجات من أجل تنفيذ البرامج بهذه اللغة (-?).

? , , Linux , . seL4 ( ) NICTA, , ( ?).

: — , , , , seL4 , . .