my first thought was something something dependent types (Idris, Agda), but it also sounds like TS-like structural typing with a Rust-like Result type. proving

my first thought was something something dependent types (Idris, Agda), but it also sounds like TS-like structural typing with a Rust-like Result type. proving that every incoming message is either parsed correctly or we return an error seems to be the basic building block. and then every transformation should be other pure functions. thought I guess you mean something more top-downish? for that there's "program interpretation" ( https://github.com/AdrielC/free-arrow https://github.com/AdrielC/free-arrow ) and this just looks very interesting https://deepai.org/publication/a-coq-based-synthesis-of-scala-programs-which-are-correct-by-construction https://deepai.org/publication/a-coq-based-synthesis-of-scal...