C*: C 언어 위에 증명을 통합해 프로그래밍과 검증을 하나로

저는 한동안 이 길을 걸어왔습니다. 저는 Ada/SPARK를 배우기로 결정했습니다. Ada 2022는 새로운 SPARK 2014 업데이트를 공급하기 시작할 것입니다. 네, 둘 다 장황합니다. 만약 당신이 그런 것을 좋아하지 않고, Pascal류의 문법을 좋아하지 않는다면요. 믿으세요, 저는 APL/J/k/uiua/BQN, Forth, ASM을 좋아합니다. 저는 보통 문법에 무관심합니다. PL과 생태계(대부분이 생각하는 것보다 더 중요합니다)가 당신의 요구를 충족시키기만 하면요. 저는 2018년에 Rust를 시도했고, 2023년에 다시 시도했지만, 매우 복잡하다는 것을 알았고, 음, 문법에 대한 호감이 없었습니다. 저는 ML이나 Haskell과 같은 문법을 더 선호했을 것입니다. Zig는 좋아 보였지만, 용도가 다르고 너무 새롭습니다. 결국, Ada/SPARK는 수십 년 동안 거대하고, 고신뢰성이며, 고안전성이 요구되는 응용 프로그램에 사용되어 왔습니다. Rust는 그들의 사랑을 일부 받고 있고, 그 반대도 마찬가지입니다. AdaCore는 검증된 Rust 컴파일러를 만들었지만, 실제 제품(Blacktail hoist)이 진행 중인 상황에서, 우리는 높은 안전성과 표준 인증을 달성하기 위해 도구 세트, 보증, 감사 용이성, 승인 용이성이 필요합니다. 항공 우주, 방위, 철도, 자동차를 생각해 보세요. 저는 1977년에 프로그래밍을 시작했기 때문에, 제 마음속에는 항상 ASM/C에 대한 자리가 있습니다. 저는 MS의 F#, F*, LOW를 사용해 보았고, 그것들은 좋지만, 그것들과 Rust는 Ada/SPARK의 실제 세계 유산을 단순히 가지고 있지 않습니다. 저는 Shen을 사용하여 소프트웨어의 덜 안전에 중요한 영역의 일부 형식적으로 검증된 모델을 작성해 왔으며, 그것이 신선하다고 생각합니다. 하지만, 제 일상 업무는 Rust가 형식적으로 검증되고 입증된 t [...]로 더 성숙해질 때까지 Ada/SPARK에 집중하는 것입니다.