Analyzing NASA's hyperspectral data to detect elements in OCaml through a type-safe, provably correct way