3 ms·
In addition to my other comment here, is there any application of formal verification for complex ETL (Data) pipelines, from the standpoint of enumerating trans
by ewuhic 3y ago
In addition to my other comment here, is there any application of formal verification for complex ETL (Data) pipelines, from the standpoint of enumerating transformations, workflow steps, and states, with less emphasis on temporal soundness?
- pas 3y agomy 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...