I've been looking at writing a code generator, which spits out vectorized code for multi-way joins (kind of like "dynamic programming" to not suffer from being locked in a specific order of binary joins), with the additional complications of being for the incremental/difference-based "Differential Dataflow"[0], the multi-temporal aspect DDFlow needs to handle it's iterative/fixpoint operator, and dynamically adjusting IO concurrency (the asymptotics of part of the "dynamic programming" index traversal suffer when squeezing concurrency out of it, as it's pretty much cache prefetching).
It's been about a year since I realized the impact of a JIT-like query compiler for these kinds of join-project queries, but needing to balance IOPS, vectorization, and likely even applying (vectorized) B-tree tactics within a 4k page, on top of the weirdness from multi-temporal (not just bi-temporal) delta-based records (~change-data-capture stream; needs to be integrated/materialized to get a point-in-time view)... sounds like a recipe for logic bugs/off-by-one errors.
They are already hard-to-impossible to notice if it'd be used in production, it being a code generator allows situations with only edge case queries having data-dependent edge case bugs, and the addition of dynamic/adaptive IO concurrency makes reproducing/debugging a detected error next to impossible.
I wouldn't dare to trust the code generator I'd write, if not formally verified. Not because I don't have faith in my skills, but because it's extremely complex code that has to be fast and fall out of a JIT and it's nature makes off-by-one errors in index access unusually likely. And debugging a known error might well be harder than formally verifying to find the bug.
TL;DR: There is code that would be useful if written, but is so complex and neigh-impossible to debug that formally verifying it might be easier than debugging it to "production-grade". I hope this project makes that kind of approach practical for those engineers who could write the code and make it pass integration tests.
It's been about a year since I realized the impact of a JIT-like query compiler for these kinds of join-project queries, but needing to balance IOPS, vectorization, and likely even applying (vectorized) B-tree tactics within a 4k page, on top of the weirdness from multi-temporal (not just bi-temporal) delta-based records (~change-data-capture stream; needs to be integrated/materialized to get a point-in-time view)... sounds like a recipe for logic bugs/off-by-one errors.
They are already hard-to-impossible to notice if it'd be used in production, it being a code generator allows situations with only edge case queries having data-dependent edge case bugs, and the addition of dynamic/adaptive IO concurrency makes reproducing/debugging a detected error next to impossible.
I wouldn't dare to trust the code generator I'd write, if not formally verified. Not because I don't have faith in my skills, but because it's extremely complex code that has to be fast and fall out of a JIT and it's nature makes off-by-one errors in index access unusually likely. And debugging a known error might well be harder than formally verifying to find the bug.
[0]: https://news.ycombinator.com/item?id=25867693 https://news.ycombinator.com/item?id=27512224
TL;DR: There is code that would be useful if written, but is so complex and neigh-impossible to debug that formally verifying it might be easier than debugging it to "production-grade". I hope this project makes that kind of approach practical for those engineers who could write the code and make it pass integration tests.