3 ms·
This article represents an ongoing trend that we've seen over the last 3 years as a resurgence in optimization techniques for directly modeling tasks which hist
by KirinDave 8y ago
This article represents an ongoing trend that we've seen over the last 3 years as a resurgence in optimization techniques for directly modeling tasks which historically were considered "not amenable to optimization techniques." We saw this last year as well with the landmark, "The Case for Learned Index Structures" [0] and in prior years with Coda Hale's "usl4j And You" [1], which can easily be woven in realtime into modern container control planes.
We've also seen research in using search and strategy based optimization techniques [2] (such as Microsoft's Z3 SMT prover[3]) to validate security models. Some folks are even using Clojure's core.logic at request time to validate requests against JWTs for query construction!
[0]: https://arxiv.org/abs/1712.01208 https://arxiv.org/abs/1712.01208
[1]: https://codahale.com/usl4j-and-you/ https://codahale.com/usl4j-and-you/
[2]: http://www0.cs.ucl.ac.uk/staff/b.cook/FMCAD18.pdf http://www0.cs.ucl.ac.uk/staff/b.cook/FMCAD18.pdf (and by the way, this made it to prod last year, so an SMT solver is validating all your S3 security policies for public access!)
[3]: https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3