| I'd usually ignore the language. Yet, given your interesting resume, there could be some practical decisions and decent code in the compiler worthy of a look in near future. ;) It indeed has some benefits from Ocaml and safer than plain C. So, good work covering that detail. I'll try to address this, though: "but when it comes to logical correctness of code I do not see amazing benefits from languages like ocaml." First, why Ocaml is good for compilers. Most of this is still true and why Rust team used it: http://flint.cs.yale.edu/cs421/case-for-ml.html What I can't overstate, already in that link, is how much easier it is to verify the properties of ML languages. They were originally designed to write a theorem prover IIRC. SML had a formal semantics for easier modeling. It allowed for functional programming style that avoids state management issues while (esp Ocaml) still lets you get hands dirty where needed. Modifications for tracking information flow, dependent types, concurrency... all sorts of things were pretty straight-forward. Had a certifying compiler early. Relevant to logical correctness, it's easier to map functional specifications to a ML than a mess like C. This was proven when people doused Leroy et al with praise over first, verified compiler for C because it really was that hard. Likewise seL4 matching functional specs to C kernel code took man-years of effort. So, languages like C are really hard to get logically correct. Languages like SML/Ocaml are pretty easy to get it done right if you understand the problem. Rarely the language causing your issues. A hybrid like a modified C or Modula that has ML-like advantages without C's disadvantages brings you closer to that ideal while preserving performance & control. |