learning #rust makes me miss linear types when i use every other language and learning #idris makes me miss totality checking and dependent types