Poor syntax errors
The error messages reported by why3 contain no context on the nature of a syntax error, which can lead to frustrating moments especially at the end of a long session. For example, a file containing:
let val () : () = 1
will report
File "../wprust/test.mlw", line 1, characters 4-7:
syntax error
the error is because val
is a reserved keyword, it would be tremendously helpful if the error mentioned something along the lines of "Found reserved keyword val
where an identifier was expected"