Исходное сообщение
"Линус Торвальдс не исключил возможность интеграции поддержки..." Отправлено Аноним, 26-Июн-22 19:34
> кто-то признал, что 100% гарантий не даст ни один ЯП Конечно не даст. В верификаторах SPARK наверняка есть ошибки, программист может "неаккуратно что написать" и бажный верификаторах пропустит дыру. Со временем вылежут и баги. > я узнал о новом для себя ЯП, который имеет смысл изучить хотя бы для кругозора Мне точно известно что версия SPARK-2021 у них получилась наконец рабочая. И компилятор GNU для ADA в 2021 году так-же наконец получился рабочим и пригодным для промышленного использования. Год прошел, а я так и не решилась что-то написать, другие задачи. Меня интересуют ответы на вопросы: 1. Насколько готовый бинарь со SPARK медленнее бинаря скомпиленого с C. 2. Задачи жесткого реального времени. В ASM и C можно рассчитать количество тактов проца необходимых для работы проги. А в SPARK  можно дать гарантии исполнения бинаря за определенное количество тактов процессора? 3. Насколько долго писать на SPARK по сравнению с C или Python? Трудозатраты?

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	>> кто-то признал, что 100% гарантий не даст ни один ЯП > Конечно не даст. В верификаторах SPARK наверняка есть ошибки, программист может "неаккуратно > что написать" и бажный верификаторах пропустит дыру. Со временем вылежут и > баги. >> я узнал о новом для себя ЯП, который имеет смысл изучить хотя бы для кругозора > Мне точно известно что версия SPARK-2021 у них получилась наконец рабочая. И > компилятор GNU для ADA в 2021 году так-же наконец получился рабочим > и пригодным для промышленного использования. Год прошел, а я так и > не решилась что-то написать, другие задачи. > Меня интересуют ответы на вопросы: > 1. Насколько готовый бинарь со SPARK медленнее бинаря скомпиленого с C. > 2. Задачи жесткого реального времени. В ASM и C можно рассчитать количество > тактов проца необходимых для работы проги. А в SPARK можно > дать гарантии исполнения бинаря за определенное количество тактов процессора? > 3. Насколько долго писать на SPARK по сравнению с C или Python? > Трудозатраты?
	Введите код, изображенный на картинке: