3 ms·
Hashlink seems to have the ambient concept of e.g. objects directly in its design and bytecode format, whereas e.g. wasm instead thinks of that in terms of "ref
by aseipp 3y ago
Hashlink seems to have the ambient concept of e.g. objects directly in its design and bytecode format, whereas e.g. wasm instead thinks of that in terms of "reference types" which represent existence of some opaque object. So there's that.
But most importantly, Neko and HashLink do not have the same kind of explicit, formally defined semantics WebAssembly has. This is a big topic but TL;DR there is a logical specification of every WebAssembly operation and behavior that all together, gives rise to a validation algorithm. This algorithm is basically a type checker, and like any type checker, it rules out bad behaviors. This validation algorithm can be run over an arbitrary WebAssembly file and tells you "yes this is valid and safe" or "no it isn't safe." By safe, that means certain behaviors are not ever possible, like stack underflow, or unstructured control flow, or that an operator is called with an invalid operand (e.g. add a string and a number). The lack of these behaviors means that when executing this program, certain isolation properties can be shown to hold -- even if the program is produced by a hostile and untrustworthy source.
That is very, very important for many use cases. Consider a browser, where it downloads a wasm file from an arbitrary server. How does it know that file was produced by a trustworthy compiler that produces correct wasm files? It can't know that. So instead it must validate the file first (according to the precise specification given by the wasm standard) before being allowed to execute it.
The validation algorithm for WebAssembly is stated in precise mathematical language, the language of type theory. And there have been several independent efforts to validate that this algorithm is correct, in machine checked theorem provers, to show that it always produces a valid yes/no answer, among all possible WebAssembly programs. Type checking and mathematical theorem proving are very closely related, in the same field, and type checking algorithms have been formalized in this manner for a very long time. So it's a well understood topic, and there is very good reason to believe the WebAssembly validation algorithm is correct and accurate (contra the oft repeated "b-b-b-but the specification might be wrong!")
If you are writing a program where the trustworthiness of the generated code isn't a problem, then you don't need that feature. For example, in the case of Haxe, you are probably producing those programs so they can be downloaded by users who already trust you, or you are compiling them directly to native executables and then giving them that. They already trust the developer to not hack their machine. In practice, some people still use WebAssembly for those use cases because it's got mindshare and a bunch of implementations, and implementing it (at a basic level) is not too difficult, and the extra security and isolation guarantees are nice to have.
- subtra3t 3y agoThanks!