>>107139732
>Isn't it easier to write verifiable software in ocaml
>Ocaml is part of a larger ecosystem of verification and theorem proving tools infact rocq is written in ocaml
>rocq can even write programs in ocaml for you
see agda and agda2hs
also check out LiquidHaskell
>Haskell is lazy which makes code higher level, but makes reasoning about termination and execution order harder.
lazy evaluation guarantees that your code will terminate if it can terminate with some evaluation order. and with pure code, execution order should not matter at all as far as the result is concerned. read more here:
https://en.wikipedia.org/wiki/Lambda_calculus
>Doesn't require monads wrappers for interfacing with c or rocq
using do notation isn't hard
>Type system is much to expressive which makes proofs a challenge for large projects as the standard way to write something in haskell may use something outside of your type restrictions
not sure what you mean
