[charon-ml] LLBC loader uses both `result` and `exception`

[niooss-ledger]

Hello,

Function crate_of_json_file is declared to return a result but may also throw some exceptions, in

charon/charon-ml/src/OfJson.ml

Lines 55 to 60 in 8547b06

	let crate_of_json_file (file : string) : (crate, string) result =
	let* format = OfPostcardBasic.format_hint_of_file file in
	match format with
	| Json ->
	let json = Yojson.Basic.from_file file in
	crate_of_json json

For example when using a malformed JSON file, Aeneas displays the raw exception with a stack trace:

$ echo '{' > /tmp/invalid.llbc
$ aeneas -backend lean /tmp/invalid.llbc 
Uncaught exception:
  
  Yojson__Common.Json_error("Line 2, bytes -1-0:\nUnexpected end of input")

Raised at Yojson__Common.json_error in file "lib/common.ml", line 5, characters 19-39
Called from Yojson__Basic.__ocaml_lex_read_json_rec in file "lib/read.mll", line 215, characters 38-57
Called from Yojson__Basic.read_json in file "lib/read.ml" (inlined), line 980, characters 3-39
Called from Yojson__Basic.from_lexbuf in file "lib/read.mll", line 875, characters 8-26
Called from Yojson__Basic.from_channel in file "lib/read.mll", line 896, characters 6-26
Called from Yojson__Basic.from_file in file "lib/read.mll", line 903, characters 14-47
Re-raised at Yojson__Basic.from_file in file "lib/read.mll", line 908, characters 6-13
Called from Charon__OfJson.crate_of_json_file in file "charon/charon-ml/src/OfJson.ml", line 59, characters 17-44
Called from Dune__exe__Main in file "Main.ml", line 557, characters 8-35

Are you interested in this kind of inconsistencies in the OCaml API? There are other occurences of similar patterns, for example when char_of_json calls String.get_utf_8_uchar.

[Nadrieril]

I have to say I'm out of my depth on how to design an OCaml library well. I hope an OCaml expert one day comes and tell me what good practice looks like so I can do that, but I can't say I care so much right now as long as my users have what they need.

[niooss-ledger]

I've read some OCaml Programming Guidelines around exceptions (https://ocaml.org/docs/guidelines#exceptions) and the documentation about Error Handling (https://ocaml.org/docs/error-handling). This last page contains an interesting quote in section Concluding Remarks:

No error handling mechanism is always better than the others, and choosing one to use should be a matter of fitting the context rather than that of taste. But opinionated OCaml code is also fine, so it's a balance.

So there no actual guidance towards exceptions or result, and I guess having functions using both exceptions and result to handle errors is actually fine so long it satisfies users' need. (It feels kind of weird, coming from C++/Rust/Python background, but I guess OCaml has its own custom ways of dealing with errors.)

Feel free to close this issue, unless you want to keep it open as a reminder to look for a review from someone familiar with good practices in OCaml libraries.

[Nadrieril]

cc @N1ark @sonmarcho do you have opinions on this topic?

[N1ark]

it would be nicer if we returned an error, i agree mixing exceptions and results is odd!