실용적인 프로그램을 만들 수는 없겠지만, Maude와 같은 정형 명세 언어도 재미있습니다. 저는 실제 코드를 쓰기 전에 데이터 흐름을 정리하고 추상화 하여 스펙을 명확히 하는데 사용합니다. 단점은 GitHub에서 무슨 언어인지 몰라서 통계가 안 잡힙니다.
@noxowlSuyeong RHIE algebraic specification language! 혹시 이거 세션 타입과도 관련이 있나요?
If you have a fediverse account, you can reply to this note from your own instance. Search https://hackers.pub/ap/notes/0195fab8-842b-7728-8e7c-f4f59a7a4f74 on your instance and reply to it.
@bglbgl gwyng 네 직접 논리를 정의해서 쓰시면 할 수 있습니다. 수업에서는 뮤텍스 프로토콜 검증을 위한 증명을 했었고요. GitHub나 논문 발표 선에서 동시성이나 암호화 관련 증명하는데 가끔 보이는 것 같습니다. 저도 인터랙션 플로우를 상상하며 정의할 때 엣지케이스를 미리 시뮬레이션(물론 현실은 쉽지 않음) 해 보는데 활용합니다.
