Previous posts in this series introduced Frml, then explained how it checks simplar scalar code, handles contracts between functions, and deals with loops. This post shows how Frml handles arrays. What We’re Doing A minimal array program is: fn main() -> Int { let a: Array<Int> = [2, 3, 5]; assert a[2] == 5; return length(a); } The array type checker subclasses the loop type checker and adds visitors for the array syntax. Everything scalar and every while loop is checked exactly as before; the new visitors only handle array nodes. Array Access visit_ExprArrayAccess checks two things: the expression being...