История изменений
Исправление hateyoufeel, (текущая версия) :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. То есть, x40 писанины. Можешь почитать про это тут.
И ещё потребовалось сделать отдельный компилятор (CompCert), для которого потребовались примерно аналогичные пруфы. Там чуть проще, потому что CompCert написан на Coq, а не C.
Во многом из-за всего этого ада, абсолютно упоротой модели выполнения у Си и чудовищной жырноты сишных компиляторов (gcc и clang уже в несколько миллионов строк кода ушли каждый) куда проще взять нормальныхй язычок и с Си вообще не связываться, если ты находишься в ситуации, когда баг в коде грозит отрывом жопы.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться, ибо они совсем не ведают что несут.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исправление hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
И ещё потребовалось сделать отдельный компилятор (CompCert), для которого потребовались примерно аналогичные пруфы. Там чуть проще, потому что CompCert написан на Coq, а не C.
Во многом из-за всего этого ада, абсолютно упоротой модели выполнения у Си и чудовищной жырноты сишных компиляторов (gcc и clang уже в несколько миллионов строк кода ушли каждый) куда проще взять нормальныхй язычок и с Си вообще не связываться, если ты находишься в ситуации, когда баг в коде грозит отрывом жопы.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться, ибо они совсем не ведают что несут.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исправление hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
И ещё потребовалось сделать отдельный компилятор (CompCert), для которого потребовались примерно аналогичные пруфы. Там чуть проще, потому что CompCert написан на Coq, а не C.
Во многом из-за всего этого ада, абсолютно упоротой модели выполнения у Си и чудовищной жырноты сишных компиляторов (gcc и clang уже в несколько миллионов строк кода ушли каждый) куда проще взять нормальных язычок и с Си вообще не связываться, если ты находишься в ситуации, когда баг в коде грозит отрывом жопы.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться, ибо они совсем не ведают что несут.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исправление hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
И ещё потребовалось сделать отдельный компилятор (CompCert), для которого потребовались примерно аналогичные пруфы. Там чуть проще, потому что CompCert написан на Coq, а не C.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться, ибо они совсем не ведают что несут.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исправление hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться, ибо они совсем не ведают что несут.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исправление hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я просто говнокодеришка на убогоньком недоязычке.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.
Исходная версия hateyoufeel, :
Интересная штука. Хотя мне показалось, что это х2 писанины.
Да, так и есть. В лучшем случае x2.
Для верификации seL4 (порядка 5к строк C) потребовалось частично написать, частично нагенерить (хачкеллом лол) около 200к строк пруфов на Isabelle. Можешь почитать про это тут.
Поэтому, когда сишники бьют себя пяткой в член и заявляют, что дескать какие-то там статические анал-лизаторы могут гарантировать отсутствие багов в их говнокоде, в первую очередь над этими сишниками надо насмехаться.
Плюс, если логически зафакапить условие корректности, то можно в некоторых случаях добиться доказательства корректности некорректного кода.
«Если написать говно, будет говно.»
Есть опыт использования?
Только хелловорлды. Я этими вещами не занимаюсь.
С другой стороны, многие вообще не парятся относительно верификации существующего кода и просто генерят сишный код из заранее написанных спеков на каком-нибудь Coq.