Hello “les chameaux” / “the camels (the animal)”.
This post will be really short.
Some gentleman posted this URL on hackernews, and it’s a collection of really great ideas about designing a new programming language:
What are the plan about OCaml evolution after the release of OCaml 5?
Thanks!
Cross-posted in https://inbox.ocaml.org/caml-list/11766ffb891975de9c58ff9bf13a0d4e60a9aa6e.camel@gnou.ch/T/#u
There was some discussion on Hacker News that I think rang quite true: this currently feels like a completely pie-in-the-sky idealistic wishlist of idealistic PL features, that doesn’t seem to be that backed by practical experience with formal verification.
IRIS and other formal verification frameworks are great, don’t get me wrong, but writing verified code is still a completely different process than writing normal code. The Rust-belt project seems to have been going on for at least 4 years, and they’re still working on the formalisation - and this is a full research lab of academics working full time on the problem.
That being said, on a related note, fellow OCamleers may be interested in Arthur Charguéraud’s CFML: Characteristic Formulae for ML framework for verifying OCaml code (I believe it’s still in development, so might not be ready for production use yet).
I recently stumbled upon it, and found that its quite nice for verifying OCaml programs and can be fit into an existing dune framework to gradually verify parts of your codebase - I’ve had a bit of fun verifying some small programs from the Containers library, although again, the process is quite different from writing code normally - 10% time is spent writing code, 90% is spent writing proofs, and don’t even get me started on trying to refactor/update programs.
Boy howdy, those must be simple programs [j/k j/k] I only mean that typically the ratio is much more lopsided.
I’m an interested but inexpert and uninvolved observer in the FV space, but is it worth mentioning in this context that both F* and Coq are in the broad OCaml ecosystem (by virtue of their implementation language and compilation targets) and already allow formally verified implementations?
In particular, from my very limited experience, F* seems to already hit many of the points on the wishlist in that doc (e.g., you can just write normal ml programs using side effects etc., or you can write formally verified programs using the fully dependent typing, and those can be used in the former, and it supports mutability idioms).