>Hypothetically some type systems could partially cover some of the things you've labelled as "no", but I'll aggressively beat you to the punch that such things are very hypothetical, except I'll be saying it with sadness and through grinding teeth, because I find it frustrating how thoroughly our environments ignore some issues like that. But that's a rant for a century I don't expect to live to see.
I'd agree with you, except that just this morning I was reading a paper about the NARCISSUS framework that can automatically generate encoders and decoders that provably conform to a given specification, and can be extended by a user without rewriting or modifying the framework itself. The authors even patched a networking stack (in MirageOS) with the not-especially-optimized ML extracted from their generated code and showed a performance hit that could be considered acceptable for real-life use cases.
With advances like this in program synthesis and formal verification, plus real progress in machine learning, it feels like we're living in the start of the age that was _supposed_ to happen during the golden age of AI.
(Excuse the gushing hyperbole. My coffee must have been stronger than usual this morning.)
I'd agree with you, except that just this morning I was reading a paper about the NARCISSUS framework that can automatically generate encoders and decoders that provably conform to a given specification, and can be extended by a user without rewriting or modifying the framework itself. The authors even patched a networking stack (in MirageOS) with the not-especially-optimized ML extracted from their generated code and showed a performance hit that could be considered acceptable for real-life use cases.
https://www.cs.purdue.edu/homes/bendy/Narcissus/
With advances like this in program synthesis and formal verification, plus real progress in machine learning, it feels like we're living in the start of the age that was _supposed_ to happen during the golden age of AI.
(Excuse the gushing hyperbole. My coffee must have been stronger than usual this morning.)