> -- Rifat писал(а):
> ...но и чтобы можно было формально доказать коррекность такой программы.Это очень интересное место. Работая с асинхронными взаимодействиями, которые по факту являются параллельными, можно заметить, что детерминированность асинхронных программ легко пропадает.

В коде это выглядит так, что обработчик сообщения понятия не имеет, кто прислал ему это сообщение. И, главное, когда. В асинхронных системах появляется категория времени, которая формализуется не знаю кем. Узнать бы. Это даст ключ к формальному доказательству правильности асинхронных программ.