Metody formalne obecne są w informatyce od jej początku, ale termin ten w inżynierii oprogramowania pojawiaja się dopiero, gdy jego burzliwy rozwój i rosnąca złożoność wywołały wyraźną potrzebę bardziej uporządkowanego i zorganizowanego podejścia do całego procesu produkcji softwaru. Już w latach sześćdziesiątych podjęto próby wskazania reguł i konstrukcji, które programista (zespół programistów) powinien stosować, a które omijać. Pojawiły się propozycje metod znanych pod chwytliwymi nazwami, jak: programowanie strukturalne (structured programming), systematyczne (rygorystyczne) programowanie (systematic (rigorous) programming), projektowanie poprzez stopniowe przekształcania opisu problemu do jego rozwiązania programistycznego (step-wise program refinement, top-down design) itp. Metody te próbowano coraz bardziej formalizować, łącząc naturalną konieczność pewnej systematyzacji inżynierskiego postępowania z pokusą wykorzystania rosnących możliwości komputerów do automatyzacji tego postępowania.

Akademickie rozważania na temat formalnych specyfikacji i weryfikacji zadań programistycznych zderzyły się z rzeczywistością końca lat siedemdziesiątych, które zwykło się uważać za lata postępującego kryzysu w dziedzinie projektowania softwaru. Właśnie wtedy zauważono ogromnie szybko wzrastające koszty oprogramowania (przy taniejącym ciągle sprzęcie) szczególnie odczuwalne w zestawieniu z jego rosnącą zawodnością. Niektóre z wielkich projektów nie zostały ukończone, mnożyły sie spektakularne przykłady błędów, które wymagały nadmiernych nakładów na ich poprawianie, a to z kolei często wprowadzało nowe usterki, nad którymi, po pewnym czasie, nikt nie panował. Szybko obliczono, że w cyklu życia oprogramowania najwięcej kosztują błędy powstające w początkowej fazie projektowania. Dlatego właśnie zainteresowano się bardzo poważnie metodami formalnymi. Wydawało się niektórym, że ich zastosowanie w praktyce może być remedium na powstałą, kryzysową sytuację. Te nadzieje były, niestety, podtrzymywne przez wiele nieodpowiedzialnych obietnic, które tworzyły niebezpieczny mit nie mający pokrycia ani w rzeczywistych możliwościach metod formalnych, ani w możliwościach dostępnej wtedy technologii komputerowej tam, gdzie metody te mogłyby mieć zastosowanie. Po kilku latach nastąpiło zniechęcenie, które utrwaliło poglądy zdecydowanie sceptyczne (nawet jeśli głośno nie wyrażane), co do praktycznej przydatności metod formalnych. Powstał zatem drugi niebezpieczny mit głoszący, że metodami tymi nie warto się poważnie zajmować.

W poniższym szkicu spróbujemy przekonać czytelnika, że odpowiednio rozważnie rozumiane metody formalne zawsze miały i mają swoje własne miejsce w całym złożonym procesie wytwarzania oprogramowania. Wskażemy na konieczne warunki, które muszą zaistnieć, żeby ich użyteczność była dostrzeżona, a w szczególności zwrócimy uwagę na potrzebę istnienia efektywnych narzędzi automatyzujących wiele żmudnych czynności w systematycznym projektowaniu. W tym kontekście pokażemy też, jak postęp technologiczny umożliwia realizację niektórych pomysłów, których (pozorna) prostota i spektakularność otrzymywanych wyników może pomóc w przełamywaniu obiegowych poglądów. Zwrócimy też uwagę na to, że metody “specjalizowane”, ograniczone do danej dziedziny zastosowań wydają się spełniać łatwiej oczekiwania odbiorców. Tę tezę zilustrujemy ogólną charakterystyką metod formalnych i stosowanych narzędzi w projektowaniu protokołów komunikacyjnych oraz wnioskami z realizacji projektu europejskiego, którego jednym z zadań było wspomagana komputerowo specyfikacja i implementacja protokołu XTP (EXpress Transport Protocol).