Я смотрю опять народ вынужденно уходит в теоретизирование.
Это хорошо, если "перед", а не "после"... :о)

Некоторый собственный опыт добавил крепости "заднего ума"...

Несколько раз я здесь хвалился и грозился выложить библиотеку поддержки АО в Си++. Но всё что-то мешало. Не "недоделанность" самого продуХта, а что-то в подсознании. Некое беспокойство. Вроде всё работает, но всё терзали какие-то смутные сомнения... :о)

Недавно, переписывая очередную версию, докопался... Причём, можно было и раньше понять и "дойти", но, пока всё это не покрутилось в "боевых условиях"...
Короче, - избегайте всего, что не поддерживается подлежащей операционной системой! Всякие налепки (на любом супер-пупер-навороченном языке), в полной мере реализовать безопасное поведение НЕ МОГУТ!
В случае с моей библиотекой вывод можно кратко сформулимровать такой:
В большинстве систем НЕ поддерживается явное сопоставление ресурса и средств монопольности их использования.
Если вы хотите создавать действительно надёжные системы - ищите средство обеспечивающие это условие.
И здесь мы снова приходим... к использовнию Оберонов, Ады (или... - Явы :о) ).
Почему? Потому, что отсутствие поддержки ОО на низком уровне (или, хотя бы, учёта ссылок) не позволяет реализовывать полностью надёжные системы.
Средства вроде boost, ACE, Loki хороши в "аккуратных" условиях "с  белыми воротничками". В условиях же, когда срок жизни объекта не обусловлен поведением ТОЛЬКО ВАШЕГО кода - Обероновско-Явовско-Адовский подход - "единственно позволительный". Иначе - ни в чём нельзя быть уверенным!
Исчё раз повторюсь: я не веду речь о "тепличных условиях", я больше говорю об "экстриме" РВ- и встроенных, автономных систем высокой надёжности.

Возвращаясь конкретно к моей библиотеке - я её полностью переписал. Но в реализации она стала ПОЛНОСТЬЮ непортруемой. ДАЖЕ на POSIX системы. Теперь использует чисто QNX-овые системные средства для увязки времён жизни объектов Си++ и примитивов и объектов операционной системы... Печально, но - хоть так. Тем более, что ни про Аду, ни про Яву, ни про (тем более Обероны!) никто у нас и слышать не желает... :о(

Что ж, - сойдёт хотя бы за ещё одно добавление в копилочку опыта... :о)

>>>По-моему, важно, что приходится объяснять, а кто и кому вопрос
>>>второй. Не хотелось бы застревать в вопросах верований.

Конечно важно именно это!
Приходится объяснять СЕМАНТИКУ языка, т.е. СМЫСЛОВОЕ ЗНАЧЕНИЕ грамматических конструкций.

Ответ на »сообщение 993« (Robin)
___________________________
По-моему, важно, что приходится объяснять, а кто и кому вопрос второй. Не хотелось бы застревать в вопросах верований.

>>>Для программирования это представляет серьезную
>>>проблему.

Проблема в том, что если даже человек не может в полной мере объяснить другому человеку семантику какой-то конструкции в языке программирования, то вряд ли какая-либо формальная система сможет сделать это лучше. Разумеется под человеком я имею в виду квалифицированного человека, а не двоечника, который сам не знает семантику оператора и поэтому не может это объяснить кому-то другому :) Можно поставить вопрос еще более резко: если, допустим, создатель языка не может объяснить семантику оператора в этом языке в полном объеме и без погрешностей, то от какой формальной системы мы можем это требовать?

Ответ на »сообщение 991« (Robin)
___________________________
>>>Если мы говорим не о формальном описании, то тогда вообще все предельно ясно. Любой человек может объяснить семантику любого языка другому человеку.
Оптимистическое верование :)
Любой человек может объяснить семантику любого языка другому человеку С НЕКОТОРОЙ ПОЛНОТОЙ И НЕКОТОРОЙ ПОГРЕШНОСТЬЮ.
Для программирования это представляет серьезную проблему.

>>>Практически требуется даже не формальное описание, а возможность
>>>согласованного взаимодействия между этими системами

Если мы говорим не о формальном описании, то тогда вообще все предельно ясно. Любой человек может объяснить семантику любого языка другому человеку. Иначе мы бы не смогли преподавать иностранные языки.

Ответ на »сообщение 989« (Robin)
___________________________
Третья система излишняя. Достаточно воспользоваться описанием двумя разными системами друг друга. Практически требуется даже не формальное описание, а возможность согласованного взаимодействия между этими системами. Я имею в виду математика и программиста.

Я не математик по образованию, но стараюсь следить за достижениями в этой области. Так вот: я еще ничего не слышал об опровержении теорем Геделя - ни первой, ни второй. А суть этих теорем, если отбросить математические "заумности" такова: ни одна формальная система не может содержать полное и формальное описание самой себя. Это доказано даже для такой "простой" формальной теории, как арифметика. Если с помощью какого-либо формального языка мы полностью и формально описали семантику другого языка, то возникает вопрос о формальном описании семантики того языка, который мы для этого использовали! Но если мы на третьем формальном языке опишем семантику второго языка, то возникает следующий вопрос - насколько формально описана его семантика! И так далее до бесконечности. Рано или поздно мы придем к тому же, к чему пришел Гедель - все формальные системы неполны по самой своей природе. Чтобы разорвать этот круг, нужен неформальный язык, т.е. человеческий.

Ответ на »сообщение 987« (captain cobalt)

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

А, понятно. Исходный текст компилятора языка написанный на нём же и есть его строгое формальное описание. Действительно, такое определение кажется вполне удовлетворительным... Правда надо ещё доказать, что компилятор компилируя любую программу на этом языке когда-нибудь всё-таки остановится. А то ведь, можно и вот такое написать:

WHILE ~найденоОпровержениеВеликойТеоремыФерма DO
  ПоискатьЕщё
END

Ответ на »сообщение 983« (Илья Ермаков)
___________________________

-- Язык для описания семантики других алгоритмических языков сам является алгоритмическим языком.

-- На любом алгоритмически полном языке можно описать семантику любого другого алгоритмического языка.

-- Машину Тьюринга можно формализовать в терминах множеств и отношений.

-- Все формальные системы основываются на аксиомах. Если имеющаяся система оказалась неполной для наших целей, всегда можно добавить аксиому по своему усмотрению. ;-)

Ответ на »сообщение 985« (Сергей Губанов)
___________________________
Как чисто формально задать правило, что идентификаторы должны быть сначало где-то определены? Как чисто формально запретить определение идентификатора если данное имя уже было определено где-то выше? Как чисто формально сказать, что переменная должна быть инициализирована перед использованием?..

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