[17:35:28] <ada_ru> (I_vlxy_I) На тему надежности: https://cakeml.org/
[17:52:48] <geniepro> ну так-то есть и верифицированный компилятор сишечки https://ru.wikipedia.org/wiki/CompCert
самый главный окамлер его сделал
[20:57:27] <ada_ru> (Максим) я не знал, что есть формальное определение языка Си
[22:44:08] <geniepro> этот компилятор не полностью совместим с си, но достаточно совместим:
CompCert C supports all of ISO C 99, with the following exceptions:
switch statements must be structured as in MISRA-C; unstructured "switch", as in Duff's device, is not supported.
longjmp and setjmp are not guaranteed to work.
Variable-length array types are not supported.
Consequently, CompCert supports all of the MISRA-C 2004 subset of C, plus many features excluded by MISRA (such as recursive functions and dynamic heap memory allocation).
Several extensions to ISO C 99 are supported:
The _Alignof operator and the _Alignas attribute from ISO C2011.
Pragmas and attributes to control alignment and section placement of global variables.