ZuriHac 2023 Videos Online

Could we at last simply let Haskell/Agda only do the declarative part, and let the runtime written by c++/rust/zig in the imperative language soup to figure out the dirty job of how to actually run them?