Wasmtime/Wasmer are both written in Rust so it was easy to integrate them. By the way, Wasm3 is an interpreter, not a JIT compiler, but this also has some use cases! For example, running an instance from “cold storage” requires a JIT compilation step which might take more time then just interpreting it. It would be cool to have a fast interpret like Wasm3 too.
We’ve created a crate “uptown_funk” which enables us to write Rust code which easily integrates with both Wasmer and Wasmtime. It was very helpful in implementing WASI and it takes a little bit different approach than Wasmer and Wasmtime. Regarding, Wasmer vs. Wasmtime, we don’t have a preference yet, both are great!
We agree with you, we are currently focused only on runtime running on an existing OS. We know there are different uses-cases so we could organize the project so that you can use what you need. In theory, you could use it right now inside of your Rust app to run plugins as Lunatic processes, but we need to document it a little bit better and maybe showcase an example.
We will take a look at embly! For Rust currently you just have to add wasm32-wasi target and compile for it. There are still some problems (WASI is not yet finished, maybe binary size could be optimized). Our current idea is to build a small cargo command which would do building and deploying. Wasmer is doing great work with tooling for other languages. We are now focused on Rust and AssemblyScript, but as Wasm and WASI mature we would like to simplify it for more languages.
We have been thinking about live process migration. I’m planning to do a demo where we run a lot of board games (e.g. chess) on authoritative servers using Lunatic. Then we give a developer ability to move a live game to a different machine without players noticing. We are still working out the details, but that area also excites us!
Factorio is a 2d game where logistics is one of the core problems players have to solve. When they implemented multiplayer they went for the "every player/server simulates the whole game perfectly deterministically"-strategy which is great imo, but it begs the question: what happens when simulations diverge? They call it Desyncronization [1], and it's considered a bug.
They had lots of desyncs at first, but nowadays Factorio is fantastically stable in this respect. One of the tools they developed for themselves to achieve this (and the reason why I'm bringing up Factorio here) is called "Heavy Mode" [2], which is a game option that saves & reloads the full game state on every tick (the game targets 60 ticks/s), and compares the before/after states for inconsistencies.
Perhaps a similar "Heavy Mode" for Wasm live migrations could aid in hardening such a feature. E.g. spawn two instances of the same process on different hosts, and migrate both to new hosts every, say, 100k instructions, comparing a hash of their serialized representations at each migration.
You are thinking in the right direction, but there are some technical differences between how NodeJS works compared to Erlang or Go. For example, in NodeJS you could accidentally block the event loop by some unintended computation, but Lunatic and Erlang periodically give control back to the runtime. We also want to abstract the syscall layer, for example, in our lunatic.run demo, you write a program which seemingly uses standard input/output but we actually read/write from a socket.
By the way, if it sounds vague, that's important info for us, we have to improve that!
I don't read it like that at all. Rust is mentioned only once. Nevertheless I do care if a tool I am considering to use is written in JavaScript, Rust or some esoteric language. It means a lot, not only for "safety" which is not important to you that much, but also for maintainability, community, and the future of the project. Of course, what triggers you probably is mentioning Rust in the title of the post. Still hard to imagine being so annoyed by it–if authors thinks it's important or it will grab attention, why not use it...
Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice.
I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".
I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men.
Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation.
Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.
UIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same.
Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.
UIP is "unicity of identity proofs". I think this will rule proofs where we wish to talk about proofs of equality of two objects. I don't know off the top of my head any math that wants to do such a thing, but I'm far from an expert.
> Why start calling things 2-vectors, when you could call them 2-forms and people would know what you were talking about?
There is more to 2-forms. Also, to be precise, they are functions from a vector space to the scalar field (usually reals). Sure, they form a (dual) vector space but I think it would be more confusing to call GA elements k-forms.
