To add to this, I think text still needs to be the canonical representation of programs. But we're still ways away with tools to express ways we want to modify, generate code. I think the late Pieter Hintjens had the right of it: we should generate code more often (I know it's polemic here). Not behind some magic curtains like the overly complex (for me) and difficult-to-inspect c++ templates but actual code generators.
One example: recordflux [0] generates, from a high-level dsl, SPARK code that can be proved to be Absent of Run-Time Error. It has a model checker for high-level constraints but lays out serialisation/deserialisation code to access fields. They've been recently working protocol/session-level modeling and it's getting very interesting.
I have a similar tool that I use to generate AORTE serdes code, but once you have that, you can go on to generate fuzzers, proxies to other techs.
We're probably also missing a way to target interesting intermediate representations of programs (either Why3 VCs, cbmc GOTO, but maybe also to lean 4 or whatever temporal logic tool of the day, or other automated/assisted proof or generation environments).
Writing those is a huge undertaking every time, and a lot of duplicated
potentially buggy effort. I look at the amazing work that's been done (and still being done) to bring up libadalang, a parsing and high level semantic query tool that changed my day-to-day coding paradigm. One of the missing pieces of the puzzle is to me the 'generic
parser and semantic specification' that would generate an interpretor and all those proxies for you.
One example: recordflux [0] generates, from a high-level dsl, SPARK code that can be proved to be Absent of Run-Time Error. It has a model checker for high-level constraints but lays out serialisation/deserialisation code to access fields. They've been recently working protocol/session-level modeling and it's getting very interesting.
I have a similar tool that I use to generate AORTE serdes code, but once you have that, you can go on to generate fuzzers, proxies to other techs.
We're probably also missing a way to target interesting intermediate representations of programs (either Why3 VCs, cbmc GOTO, but maybe also to lean 4 or whatever temporal logic tool of the day, or other automated/assisted proof or generation environments).
Writing those is a huge undertaking every time, and a lot of duplicated potentially buggy effort. I look at the amazing work that's been done (and still being done) to bring up libadalang, a parsing and high level semantic query tool that changed my day-to-day coding paradigm. One of the missing pieces of the puzzle is to me the 'generic parser and semantic specification' that would generate an interpretor and all those proxies for you.
[0] https://blog.adacore.com/recordflux-from-message-specificati...