AI가 형식 검증을 주류로 만들 것이다
------------------------------
- *형식 검증(formal verification)* 은 코드가 명세를 항상 만족함을 수학적으로 증명하는 방법으로, 오랫동안 연구 중심의 한정된 영역에 머물러 있었음
- seL4 마이크로커널 등 일부 대형 시스템이 형식 검증으로 개발되었지만, *높은 난이도와 비용* 때문에 산업 현장에서는 거의 사용되지 않았음
- 최근 *LL…
------------------------------
https://news.hada.io/topic?id=25129&utm_source=googlechat&utm_medium=bot&utm_campaign=1834
If you have a fediverse account, you can quote this note from your own instance. Search https://sns.lemondouble.com/notes/agcy89gnx4 on your instance and quote it. (Note that quoting is not supported in Mastodon.)
구현 중인 린터의 코드 수정 제안 기능에 부분적으로 한번 형식 증명을 적용해볼만 할 것 같기도 하다