> Но математическое обоснование должно же, по идее, подразумевать существование (корректной и полной)
> модели железа, на котором это будет крутиться? Что, понятное дело, нереально.Не должно. :)
В идеале так надо было бы, конечно. Но если играть в идеалистов, то вообще не стоит браться за написание программ, потому что никто не знает как писать программы без багов. В общем, если мы позиционируем себя как практиков, то мы должны признать, что неполная модель железа использованная в доказательстве, всё же лучше чем отсутствие этой самой модели. Правда да, тесты позволяют протестировать что-либо на реальном железе, но меня если честно, сильно сомневает способность тестов выявить какую-то "железную" проблему. Разве что документированную, многократно описанную, с существующим эксплоитом в паблике.
Собственно:
> Hardware management: the proof tries to make only the most minimal assumptions on the underlying
> hardware. It abstracts from cache consistency, cache colouring and TLB (translation lookaside
> buffer) management. The proof assumes these functions are implemented correctly in the assembly
> layer mentioned above and that the hardware works as advertised. The proof also assumes that
> especially these three hardware management functions do not have any effect on the behaviour of
> the C program. This is only true if they are used correctly.
Взято отсюда: http://ertos.nicta.com.au/research/l4.verified/proof.pml
Причём эта ссылка достаточно древняя, например, сейчас они уже не доверяют компилятору, и проверяют также и сгенерированный машинный код на корректность: http://www.techworld.com.au/article/547841/nicta_release_dro...
> То есть, вероятно, математические доказательства корректности - это интересное
> упражнение, но для практики не больше ли пользы в хорошем покрытии юнит-тестами и
> основательном объеме fuzzy-тестирования?
Нет, математическое доказательство полезнее. Потому что оно работает не с конкретными наборами входных данных, а с множествами этих самых наборов. Представь себе, в качестве примера, функцию высчитывающую корни квадратного уравнения, которая на входе принимает три числовых значения, на выходе даёт 0, 1 или 2 числовых значения. Сколько разных случаев можно проверить тестом? 5? 10? 100? 1000? 10000? Математически же можно проверить все возможные случаи, несмотря на то, что количество этих случаев, равно бесконечности (практической бесконечности, поскольку все случаи проверить практикой невозможно).
Конечно есть свои нюансы. Для того, чтобы доказать функциональную корректность кода, требуется предварительно написать спецификацию этого кода на формальном языке. Спецификация тоже может содержать ошибки. Но, поскольку и тесты также могут содержать ошибки, это нельзя считать недостатком метода по сравнению с написанием тестов.
А вообще, это весьма перспективное направление. Варнинги компилятора придумали давно. Потом кому-то их показалось мало, и создали статистические анализаторы. Ребятам же показалось мало проверки кода по паттернам, и они попытались решить общий случай. Это следующая итерация того же самого. Которая сейчас лишь пытается взлететь, но когда взлетит и войдёт в обыденность, её уже будут вытеснять системы автоматического написания программ по спецификациям. И вот тогда, востребованность программистов на рынке труда упадёт ниже плинтуса, и останутся одни быдлокодеры, а настоящие программисты вымрут как динозавры.
