Czy ktoś widział produkcyjne użycie języków ogólnego przeznaczenia z formalna weryfikacją kodu jak Idris, Idris2 czy Kind?

Ujął w temacie

Nie

Nie do końca to samo, ale SPARK jest używany.

Formalna weryfikacja kodu jak najbardziej jest stosowana w przemyśle.

Satanistyczny Awatar napisał(a):

Formalna weryfikacja kodu jak najbardziej jest stosowana w przemyśle.

Ale jak to wygląda, jak to działa? Czy mogę sobie napisać interpeter BrainFucka weryfikowanego formalnie?

BTW We wtorek byłe na Monadic Warsaw i gościu mówił że napisał Aplikację webową w pseudo ELM który tak naprawdę był Coq, z którego wyeksportował kod do Ocamla, który to następnie skompilował do JSa za pomocą BucketScript i w rezultacie miał licznik pracujący w przedziale 1-10 zweryfikowany formalnie. Więc za się stworzyć normalną aplikację w coqu a potem eksportować do innych języków jak Haskell, OCaml itp

BTW2 Po spotkaniu przypomniało mi się że kiedyś już znalazłem coś takieog jak LiquidHaskell tylko o tym zapomianiełem. Czyli można by mieć Haskella weryfikowanego :D Jedyny problem że składnia LiquidHaskell trochę mi przypomina adnotację w Javie :P ciekawe czy może dojść do tego że będę miał więcej kody w adnotacjach niż w normalnym Haskellu. Jak w starej dobrej Javie :D