Frml: Next Steps

Previous posts in this series introduced Frml, explained how it checks simplar scalar code and handles contracts between functions, and then discussed how it deals with loops, checks arrays, and checks built-in functions. The final language level, complete, doesn’t add any new features. Instead, it serves as a placeholder in case we want to extend the language further. I’m not going to do this myself, but if you are a student (or a professor looking for projects for students) please get in touch. Algebraic Data Types and Pattern Matching Add enum sum types and a match expression to teach structural induction over data and Z3’s datatype theory. A sample program would be: enum Option<T> { None, Some(T) } fn get_or(a: Option<Int>, d: Int) -> Int ensures result == d or result != d { match a { None => d, Some(v) => v, } } Frml currently proves things about numbers and arrays but never about the shape of a value. Lists, options, and trees are where induction over data structures becomes…