Могат ли функциите на Haskell да бъдат доказани/проверени чрез модел/потвърдени със свойства за коректност?

Е, няколко неща, с които да започнете, тъй като поемате по пътя на Haskell:

• Запознати ли сте с кореспонденцията между Къри и Хауърд? Има системи, използвани за машинно проверени доказателства, базирани на това, които в много отношения са просто функционални езици за програмиране с много мощни типови системи.

• Запознати ли сте с областите на абстрактната математика, които предоставят полезни концепции за анализиране на код на Haskell? Различни разновидности на алгебрата и някои части от теорията на категориите се появяват много.

• Имайте предвид, че Haskell, както всички езици, пълни с Turing, винаги има възможност за непрекратяване. Като цяло е много по-трудно да се докаже, че нещо винаги ще бъде вярно, отколкото да се докаже, че или нещо ще е вярно, или ще зависи от непреходна стойност.

Ако сериозно търсите доказателство, а не просто тестване, това са нещата, които трябва да имате предвид. Основното правило е следното: Накарайте невалидните състояния да причинят грешки на компилатора. Първоначално предотвратете кодирането на невалидни данни, а след това оставете програмата за проверка на типа да свърши досадната част вместо вас.

Ако искате да отидете още по-далеч, ако паметта не ме лъже, асистентът за доказателство Coq има „екстракт от Haskell", която ще ви позволи да докажете произволни свойства за критични функции, след което да превърнете доказателствата в код на Haskell.

За извършване на фантастични системни неща директно в Haskell, Олег Кисельов е Великият майстор. На неговия сайт можете да намерите примери за хитри трикове като полиморфни типове от по-висок ранг за кодиране на статични доказателства за проверка на границите на масив.

За по-леки неща можете да правите неща като използвайки сертификат на ниво тип, за да маркирате част от данните като проверени за коректност. Вие все още сте сами за самата проверка на коректността, но друг код може поне да разчита на знанието, че някои данни всъщност са били проверени.

Друга стъпка, която можете да предприемете, изграждайки лека проверка и фантастични системни трикове, е да използвате факта, че Haskell работи добре като хост език за вграждане на специфични за домейна езици; първо конструирайте внимателно ограничен подезик (в идеалния случай такъв, който не е пълен по Тюринг), за който можете по-лесно да докажете полезни свойства, след това използвайте програми в този DSL, за да предоставите ключови части от основната функционалност във вашата цялостна програма. Например, бихте могли да докажете, че функция с два аргумента е асоциативна, за да оправдаете паралелно намаляване на колекция от елементи, използващи тази функция (тъй като подреждането на приложението на функцията няма значение, а само подреждането на аргументите).

О, едно последно нещо. Няколко съвета за избягване на капаните, които Haskell наистина съдържа, които могат да саботират код, който иначе би бил безопасен чрез конструиране: Вашите заклети врагове тук са общата рекурсия, IO монадата и частични функции:

• Последното е относително лесно да се избегне: не ги пишете и не ги използвайте. Уверете се, че всеки набор от съвпадения на шаблони обработва всеки възможен случай и никога не използвайте error или undefined. Единствената трудна част е избягването на стандартни библиотечни функции, които могат да причинят грешки. Някои очевидно не са безопасни, като fromJust :: Maybe a -> a или head :: [a] -> a, но други може да са по-фини. Ако откриете, че пишете функция, която наистина, наистина не може да направи нищо с някои входни стойности, тогава вие позволявате невалидните състояния да бъдат кодирани от типа вход и първо трябва да поправите това.

• Второто е лесно да се избегне на повърхностно ниво чрез разпръскване на неща чрез различни чисти функции, които след това се използват от IO израз. По-добре е, доколкото е възможно, да преместите цялата програма в чист код, така че да може да бъде оценена независимо с всичко, освен с действителния I/O. Това най-вече става трудно само когато имате нужда от рекурсия, управлявана от външен вход, което ме отвежда до последния елемент:

• Думи за мъдрите: Добре обоснована рекурсия и продуктивна ядрена курсия. Винаги се уверявайте, че рекурсивните функции или преминават от някаква начална точка към известен базов случай, или генерират поредица от елементи при поискване. В чистия код най-лесният начин да направите това е или чрез рекурсивно свиване на крайна структура от данни (напр. вместо функция, която се извиква директно, докато увеличава брояч до някакъв максимум, създайте списък, съдържащ диапазона от стойности на брояча, и го сгънете ) или рекурсивно генериране на мързелива структура от данни (напр. списък с прогресивни приближения към някаква стойност), като същевременно внимателно никога не смесвате двете директно (напр. не просто „намерете първия елемент в потока, отговарящ на някакво условие“; може да не Вместо това вземете стойности от потока до някаква максимална дълбочина, след това потърсете в крайния списък, като обработите по подходящ начин ненамерения случай).

• Комбинирайки последните два елемента, за частите, където наистина се нуждаете от IO с обща рекурсия, опитайте се да изградите програмата като инкрементални компоненти, след което кондензирайте всички неудобни битове в една функция "драйвер". Например, можете да напишете GUI цикъл на събития с чиста функция като mainLoop :: UIState -> Events -> UIState, тест за излизане като quitMessage :: Events -> Bool, функция за получаване на чакащи събития getEvents :: IO Events и функция за актуализиране updateUI :: UIState -> IO (), след което всъщност да стартирате нещото с обобщена функция като runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). Това поддържа сложните части наистина чисти, като ви позволява да изпълнявате цялата програма със скрипт за събитие и да проверявате полученото състояние на потребителския интерфейс, като същевременно изолирате неудобните рекурсивни I/O части в една абстрактна функция, която е лесна за разбиране и често неизбежно ще бъде правилна от parametricity.

Вероятно най-близкото нещо до това, което питате, е Haskabelle, инструмент, който идва с асистента за доказване Isabelle, който може да превежда файлове на Haskell в теориите на Изабел и ви позволява да докажете неща за тях. Доколкото разбирам, този инструмент е разработен в рамките на проекта HOL - ML - Haskell и страницата с документация съдържа малко информация за теорията зад нея.

Не съм много запознат с този проект и не знам много какво е направено с него. Но знам, че Брайън Хъфман си играе с тези неща, вижте документите му и разговори, те трябва да съдържат подходящи неща.

Не съм сигурен дали това, което искаш, наистина ще те направи щастлив. :-)

Проверката на модела на език с общо предназначение е почти невъзможна, тъй като моделите трябва да са специфични за домейна, за да бъдат практични. Поради теоремата за непълнотата на Гьодел, просто няма няма метод за автоматично намиране на доказателства в достатъчно изразителна логика.

Това означава, че трябва сами да пишете коректури, което повдига въпроса дали усилията си заслужават отделеното време. Разбира се, усилията създават нещо много ценно, а именно увереността, че вашата програма е правилна. Въпросът не е дали това е задължително, а дали отделеното време е твърде голям разход. Работата с доказателствата е, че докато може да имате "интуитивно" разбиране, че програмата ви е правилна, често е много трудно да формализирате това разбиране като доказателство. Проблемът с интуитивното разбиране е, че е силно податлив на случайни грешки (печатни и други глупави грешки). Това е основната дилема при писането на правилни програми.

Така че изследването на коректността на програмите е свързано с улесняване на формализиране на доказателства и автоматична проверка на коректността им. Програмирането е неразделна част от "лекотата на формализиране"; много е важно да пишете програми в стил, който е лесен за разсъждение. В момента имаме следния спектър:

• Императивен език като C, C++, Fortran, Python: Много е трудно да се формализира нещо тук. Единичните тестове и общите разсъждения са единственият начин да получите поне някаква увереност. Статичното писане улавя само тривиални бъгове (което е много по-добре, отколкото да не ги улавя!).

• Чисто функционални езици като Haskell, ML: Expressive type system помага за улавяне на нетривиални бъгове и грешки. Доказването на правилността на ръка е практично за фрагменти до някъде около 200 реда, бих казал. (Направих доказателство за моя оперативен пакет, например.) Quickcheck тестването е евтин заместител на формализираните доказателства.

• Зависимо въведени езици и асистенти за доказателство като Agda, Epigram, Coq: Доказването на правилността на цели програми е възможно благодарение на автоматизирана помощ с формализиране и откриване на доказателство. Тежестта обаче все още е голяма.

По мое мнение, текущото сладко място за писане на правилни програми е чисто функционалното програмиране. Ако животите зависят от правилността на вашата програма, по-добре преминете ниво по-високо и използвайте асистент за доказване.

Звучи сякаш искате ESC/Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

О, и Agda вече има уеб рамка (поне доказателство за концепцията): http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

Разгледахте ли Quickcheck? Може да предложи някои от нещата, от които се нуждаете.

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

Вашият привидно прост пример, add(a,b), всъщност е труден за проверка - плаваща запетая, препълване, препълване, прекъсвания, проверен ли е компилаторът, проверен ли е хардуерът и т.н.

Навик е опростен диалект на Haskell, който позволява доказване на свойствата на програмата.

Hume е език с 5 нива, всяко по-ограничено и следователно по-лесно за проверка:

Full Hume
  Full recursion
PR−Hume
  Primitive Recursive functions
Template−Hume
  Predefined higher−order functions
  Inductive data structures
  Inductive  Non−recursive first−order functions
FSM−Hume
  Non−recursive data structures
HW−Hume
  No functions
  Non−recursive data structures

Разбира се, най-популярният метод днес за доказване на свойствата на програмата е модулното тестване, което осигурява силни теореми, но тези теореми са твърде специфични. "Типове, считани за вредни", Пиърс, слайд 66

Разгледайте Zeno. Цитирам wiki страницата:

Zeno е автоматизирана система за доказване на свойствата на програмата на Haskell; разработен в Imperial College London от William Sonnex, Sophia Drossopoulou и Susan Eisenbach. Той има за цел да реши общия проблем с равенството между два члена на Haskell за всяка входна стойност.

Много инструменти за проверка на програмата, налични днес, са от сорта за проверка на модели; в състояние да прекоси много голямо, но ограничено пространство за търсене много бързо. Те са много подходящи за проблеми с голямо описание, но без рекурсивни типове данни. Zeno от друга страна е проектиран да доказва индуктивно свойства в безкрайно пространство за търсене, но само тези с малка и проста спецификация.

Някои съвсем скорошни усилия на MSR Cambridge: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

Инструментът AProVE е (поне) в състояние да докаже прекратяване на Haskell програми, което е част от доказването коректност. Повече информация можете да намерите в този документ (по-кратка версия).

Освен това може да се интересувате от зависими типове. Тук системата от типове е разширена и използвана, за да направи невъзможни грешни програми.

Можете да използвате инструмента hs-to-coq, за да конвертирате Haskell най-вече автоматично в Coq и след това да използвате пълната мощност на асистента за доказване на Coq за проверка на вашия Haskell код. Вижте документите https://arxiv.org/abs/1803.06960 и https://arxiv.org/abs/1711.09286 за малко повече информация.