Previous posts in this series introduced Frml, then explained how it checks simplar scalar code, handles contracts between functions, deals with loops, and checks arrays. This post shows how Frml handles built-in functions like push and pop. Here’s an example program to motivate the discussion: fn main() -> Int { let a: Array<Int> = [1]; push(a, 2); assert length(a) == 2; return 0; } Built-in Functions Frml’s built-in functions live in frml/builtins.py: read(path: String) -> String returns the contents of a file write(path: String, text: String) writes text to a file print(text: String) writes text to standard output split(text: String,...