На чем пишется софт для КА?

[bsdv]

Так вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное.

Да нет, все решаемо. Другое дело, что ни в С++, ни в Джаве, ни в C# нет для этого необходимого инструментария. В результате в больших проектах (даже без "космических" требований по надежности!) приходится в начале каждой процедуры выполнять проверку всех указателей на ноль. Потому что даже если сейчас требованеие ненулевых указателей выполняется, то в дальнейшем где-то в другом месте программы другим человеком поменяется спецификация, на вход придет ноль и получится креш. А можно было бы иметь специальный тип указателей, котрые не могут быть рвны нулю. В этом стучае мы получим сообщение еще на стадии компиляции программы, что код стал некорректным. И так же по многом другим типовым источникам ошибок. К сожалениею, существующие языки программирования на безошибочное программирование совершенно не заточены. Если брать те же указатели, в распространенных языках специфицировать, что такой-то указатель не может быть нулем невозможно. И когда действительно требуется безошибочность приходится путем титанических усилий выверять код по спецификации. Вручную, очень трудоемко. Хотя это вполне мог бы делать компилятор при наличии специального языка программирования.

Пользуйтесь COM интерфейсами, иногда помогает

[yos]

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

Ну так об этом и речь. Оптимизации в компиляторе это одно, они не касаются программиста. А вот за хороший по сложности алгоритм отвечает человек. Об этом выше и шла речь.

[yos]

Так вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное.

Да нет, все решаемо. Другое дело, что ни в С++, ни в Джаве, ни в C# нет для этого необходимого инструментария.

Мы, думаю, чуть-чуть о разном говорим. Дело не в языках, а в том, что разработать логико-математическую теорию указателей, которая могла бы служить формальной системой для верификации программ, очень сложно. А то, что ведутся попытки усовершенствовать языки, сделав их более устойчивыми к ошибкам человека, то это другая история. Но все эти изменения в языках означают изменения в их семантике, как ваш пример с непустыми указателями (кстати, наверное не поможет). А "хорошая" семантика возможно позволит на её основе применить один из форм. методов. Так что всё связано довольно сложным образом.

[Александр Куприянов]

yos пишет:
 "Выдумывать" языки нужно будет ещё очень долго! Развитие языков дос их пор активно продолжается. А всё потому, что языки очень разные. А споры об этом действительно умиляют: "мне нравится этот язык, а мне тот". Это всё очень поверхностные и субьективные оценки. Суть в том, что языки разрабатывают не только, чтобы людям было приятно или легко с ними работать, а главное, особенно в случае с КА и прочей техникой, чтобы иметь "правильную" и понятную семантику. "
Конешно, языки (программирования) возникают по технологическим причинам, а возникнув, как и естественные, живут и умирают вместе с сообществом - носителем...

[sychbird]

К сожалению не помню точных ссылок, но в свое время мне попадались в материалах по  машинному переводу сведения о  якобы доказательствах вроде методами матлогики, ЕМНИП, принципиальной неосуществимости однозначности на семантическом уровне.

[Вадим Семенов]

Так вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное.

Да нет, все решаемо. Другое дело, что ни в С++, ни в Джаве, ни в C# нет для этого необходимого инструментария. В результате в больших проектах (даже без "космических" требований по надежности!) приходится в начале каждой процедуры выполнять проверку всех указателей на ноль. Потому что даже если сейчас требованеие ненулевых указателей выполняется, то в дальнейшем где-то в другом месте программы другим человеком поменяется спецификация, на вход придет ноль и получится креш. А можно было бы иметь специальный тип указателей, котрые не могут быть рвны нулю. В этом стучае мы получим сообщение еще на стадии компиляции программы, что код стал некорректным. И так же по многом другим типовым источникам ошибок. К сожалениею, существующие языки программирования на безошибочное программирование совершенно не заточены. Если брать те же указатели, в распространенных языках специфицировать, что такой-то указатель не может быть нулем невозможно. И когда действительно требуется безошибочность приходится путем титанических усилий выверять код по спецификации. Вручную, очень трудоемко. Хотя это вполне мог бы делать компилятор при наличии специального языка программирования.

А причем тут нулевые указатели? Это лишь частный случай проблемы.

Конечно. Я ее и рассотрел, как частный случай для иллюстрации основной мысли.

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

Согласен, я о том и писал. Существующие языки программирования не предоставляют надлежащей типизации. (Хотя только лигь типизацией вопрос не исчерпывается). Отдельные здравые вещи попадаются в малоиспользуемых языках типа Эйфеля и Ады, но в полной мере, пожалуй, не удоволетворяет никто.

[Вадим Семенов]

Пользуйтесь COM интерфейсами, иногда помогает

При чем тут СОМ интерфейсы?

[yos]

К сожалению не помню точных ссылок, но в свое время мне попадались в материалах по  машинному переводу сведения о  якобы доказательствах вроде методами матлогики, ЕМНИП, принципиальной неосуществимости однозначности на семантическом уровне.

Однозначности чего? Семантика -- хорошо развитая область теоретической информатики, успешно достигнуты многие результаты. И всё там однозначно потому, что формально.
Другое дело, что некоторые вещи вообще трудно формализировать, например указатели и ОО. Но попытки ведутся, некоторые довольно таки успешные, другие -- нет.

[bsdv]

Пользуйтесь COM интерфейсами, иногда помогает

При чем тут СОМ интерфейсы?

Физически не дают убить данные, пока их кто-нибудь использует. Всех проблем динамических объектов эта технология конечно не решает, но их количество  все же уменьшается. По-крайней мере отпадает надобность в повторной  проверке указателей .

[yos]

Мы ведём речь о вещах на более низком уровне абстракции.

[bsdv]

Мы ведём речь о вещах на более низком уровне абстракции.

Ну куда уж ниже. Есть задачи, которые возможно решить на уровне компиляции, есть задачи, принципиально не решаемые на этом этапе. С этим надо смириться. Отсюда растут ноги у динамических типов данных, со всеми их достоинствами и недостатками. С недостатками стараются бороться, придумывая различные технологии - вроде управления жизненным циклом объектов(данных).
Но честно говоря, жизненно важные функции управления техническими объектами ( по-крайней мере те- с которыми мне приходилось встречаться) имеют конечную размерность исходных/вычислительных данных, обусловленную конечными техническими  возможностями иформационно-измерительной части самой техники, что при условии достаточности вычислительных мощностей (главным образом памяти) вполне позволяет обходиться без этих программистских изысков.

[Agent]

П.С. Чтобы было понятней: как говорил Дейкстра, тесты могут указать только на наличие ошибок в программе, а не на их отсутствие. А вот формальные методы как раз на отсутствие. Что не значит, что тесты не нужны или неполезны.

Все ити попытки формализации тихонько зачахли еще лет 20 назад. Вместе с попытками написать ИИ. Язык программирования роли не играет. Так же как и язык общения. Написание программы - это правильный подбор кадров и правильная организация техпроцесса.

[Вадим Семенов]

Физически не дают убить данные, пока их кто-нибудь использует. Всех проблем динамических объектов эта технология конечно не решает, но их количество  все же уменьшается.

Ну этого недостаточно. Указатель изначально может быть нулевым. Кроме того он и полезен иногда нулевым, обозначающим отсутствие объекта. Нужно ведь не запретить нулевые указатели в принципе, а отлавливать возможные проблемы.

[Вадим Семенов]

Но честно говоря, жизненно важные функции управления техническими объектами ( по-крайней мере те- с которыми мне приходилось встречаться) имеют конечную размерность исходных/вычислительных данных, обусловленную конечными техническими  возможностями иформационно-измерительной части самой техники, что при условии достаточности вычислительных мощностей (главным образом памяти) вполне позволяет обходиться без этих программистских изысков.

Я тоже так думаю, но указатели это только частный случай. Могут быть и другие потенциально уязвимые места, например, переполнение, которое однажды сгубило Ариан-5

[Вадим Семенов]

Все ити попытки формализации тихонько зачахли еще лет 20 назад. Вместе с попытками написать ИИ. Язык программирования роли не играет. Так же как и язык общения. Написание программы - это правильный подбор кадров и правильная организация техпроцесса.

Да, к сожалению, дело пошло по пути грубой силы, увеличения трудоемкости и стоимости, вместо устранения причин. Ну может быть разработка софта не самая большая статья расходов и экономить нужды нет.

[bsdv]

Физически не дают убить данные, пока их кто-нибудь использует. Всех проблем динамических объектов эта технология конечно не решает, но их количество  все же уменьшается.

Ну этого недостаточно. Указатель изначально может быть нулевым. Кроме того он и полезен иногда нулевым, обозначающим отсутствие объекта. Нужно ведь не запретить нулевые указатели в принципе, а отлавливать возможные проблемы.

Насколько я понимаю, главная проблема заключается в том, что данные, на которые ссылается ваш указатель, могут быть уничтожены участком кода, не подозревающем об необходимости их дальнейшего использования. Поэтому в COM технологии одним из ключевых столпов является подсчет самим объектом  используемых ссылок на свою сущность. При этом ведется счет необнуленых ссылок, и объект сможет вызвать свой метод Destroy (другими словами освободить занимаемую им память) только если в коде больше не осталось указателей (ссылок) на него самого.

Но, как я уже говорил, это не единственная проблема...

[bsdv]

Но честно говоря, жизненно важные функции управления техническими объектами ( по-крайней мере те- с которыми мне приходилось встречаться) имеют конечную размерность исходных/вычислительных данных, обусловленную конечными техническими  возможностями иформационно-измерительной части самой техники, что при условии достаточности вычислительных мощностей (главным образом памяти) вполне позволяет обходиться без этих программистских изысков.

Я тоже так думаю, но указатели это только частный случай. Могут быть и другие потенциально уязвимые места, например, переполнение, которое однажды сгубило Ариан-5

Ну это уже более простой вопрос- вопрос корректной фильтрации измерительных данных, вкупе с вопросом размерности переменных. Вот тут уж формальным методам есть где разгуляться

[Agent]

Все ити попытки формализации тихонько зачахли еще лет 20 назад. Вместе с попытками написать ИИ. Язык программирования роли не играет. Так же как и язык общения. Написание программы - это правильный подбор кадров и правильная организация техпроцесса.

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

Причина в другом - из линейного выполнения, ветвления, цикла и разновидностей оных больше ничего не выжмешь. Попытки формализации (написать программу которая пишет программу) уперлась в ту же проблему что и "генераторы текстов" - "Война и Мир" никак не получается. Пиши хоть в машинных кодах хоть на чем то прологообразном - принципы в основе те же. Точно так же как ученые и инженеры могут делать свое дело на русском, китайском, английскои м тд. Попытки в свое время создать суперязык общения разбились о ту же проблему - не в языке дело.

[bsdv]

Все ити попытки формализации тихонько зачахли еще лет 20 назад. Вместе с попытками написать ИИ. Язык программирования роли не играет. Так же как и язык общения. Написание программы - это правильный подбор кадров и правильная организация техпроцесса.

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

Причина в другом - из линейного выполнения, ветвления, цикла и разновидностей оных больше ничего не выжмешь. Попытки формализации (написать программу которая пишет программу) уперлась в ту же проблему что и "генераторы текстов" - "Война и Мир" никак не получается. Пиши хоть в машинных кодах хоть на чем то прологообразном - принципы в основе те же. Точно так же как ученые и инженеры могут делать свое дело на русском, китайском, английскои м тд. Попытки в свое время создать суперязык общения разбились о ту же проблему - не в языке дело.

Осмелюсь предположить, что дело в интеллекте

[Agent]

Осмелюсь предположить, что дело в интеллекте

Типа того. Поэтому программисты и получают так много. Всмысле те кто умеют писать программы. А когда задача такова, что каждый потребленный милливатт стоит дороже годовой зарплаты лучшего программиста, то код будет на ассемблере, оптимален и без ошибок. Несмотря на примитивность языка.