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

Н. Вирт в статье "Хорошие идеи: взгляд из Зазеркалья" пишет: "Много лет спустя некоторые разработчики все чаще стали утверждать, что функциональные языки являются наилучшим средством для введения параллелизма - хотя было бы более уместно сказать "для облегчения работы компиляторов по определению возможностей распараллеливания программ". Вообще-то относительно несложно определить, какие части выражения могут вычисляться параллельно. Более важно то, что параллельно могут вычисляться параметры вызываемой функции, если запрещены побочные эффекты - которые не могут возникать в истинно функциональном языке. В то время, как это обстоятельство может быть истинным и, возможно, минимальным преимуществом функциональных языков, объектно-ориентированный подход предлагает более эффективный способ хорошего использования параллелизма, когда поведение каждого объекта представляется в виде отдельного процесса. ".

Меня заинтересовала фраза "объектно-ориентированный подход предлагает более эффективный способ хорошего использования параллелизма, когда поведение каждого объекта представляется в виде отдельного процесса" и у меня есть несколько вопросов:
1) реализован ли данный подход где-нибудь?
2) если да, то позволяет ли данный подход формально доказывать корректность программ?
3) если не позволяет, то есть ли другие методы параллелизма, которые можно реализовать и при этом формально доказывать корректность таких программ.