withtypes

Fly.io is doing cool stuff! We will try out their platform to deploy Lunatic to the edge.

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!

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 beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?

> 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.

I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".

I don't understand what "LEM is false" means. What are your starting assumptions that lead to the "LEM is false" conclusion? You can use/assume LEM in your system or not, most mathematicans assume LEM (without even thinking about it).

I also think that this point should be emphasized more. It helped me a lot when I realized it. I also liked the abstract approach to vector spaces. Of course, a matrix is just one way to represent linear transformations and it can also represent other things like a system of linear equations.