Hi, The following has been bugging me for a while: Avail’s type system is not sound in the present of semantic restrictions. I could be wrong of course :)
Blurp lifted from: https://developers.google.com/v8/experiments <https://developers.google.com/v8/experiments> "Soundness is a formal correctness property of a type system. It guarantees that (1) an expression that has a static type T can never evaluate to a value that is not a T, and that (2) evaluation cannot run into unexpected runtime type errors”. Not so with Avail’s semantic restrictions. I’m pretty sure when Avail is compared to other strongly-typed languages, Avail's soundness will be a big discussion topic. (Especially when we release the "Language Feature Comparison Matrix”). So it is claimed that soundness potentially allows for better optimisations, as certain properties will be statically *proven* to be true. In contrast, Avail has to resort to VM runtime optimisations: it has to guess and construct the *real* types at runtime in order to be efficient (like the Self, Smalltalk, Lua and Javascript VMs). But does that really matter? Sure, non-soundness makes it hard for the Avail's runtime to be as efficient as - say the JVM. The good thing is that with semantic restrictions we gain much more power at compile time: Avail can reject programs at a much more sophisticated level than any other programming language to date. But Avail also allows you to strengthen types at compile time that don’t hold up at runtime. Of course, nothing prevents us from adding a (very advanced) semantic restriction checker that is sound and doesn’t get in the way. But that time is not there yet. I guess it is all about trade-offs. cheers, Robbert.
signature.asc
Description: Message signed with OpenPGP using GPGMail
