История изменений
Исправление Freyr69, (текущая версия) :
Ада, мало того, что мертва, не обладает даже намеком на систему lifetime-ов.
Настолько мертва, что из альтернатив спарку только Frama-c. Но ада всяко приятнее сишки (ибо типы, параметрический полиморфизм вместо void, триплеты хоара, объекты, RAII), да и с доказательствами в ней намного проще, особенно начиная с Ada2012/Spark2014, где завезли hoare logic искаробочный. Вряд ли в ближайшее время аду что-нибудь заменит, разве что всякие Fstar с Kremlin дорастут.
Исходная версия Freyr69, :
Ада, мало того, что мертва, не обладает даже намеком на систему lifetime-ов.
Настолько мертва, что из альтернатив спарку только Frama-c. Но ада всяком приятнее сишки (ибо типы, параметрический полиморфизм вместо void, триплеты хоара, объекты, RAII), да и с доказательствами в ней намного проще, особенно начиная с Ada2012/Spark2014, где завезли hoare logic искаробочный. Вряд ли в ближайшее время аду что-нибудь заменит, разве что всякие Fstar с Kremlin дорастут.