ATS-Postiats
wasmtime
Our great sponsors
ATS-Postiats | wasmtime | |
---|---|---|
18 | 172 | |
349 | 14,407 | |
- | 2.8% | |
0.0 | 10.0 | |
about 1 year ago | 7 days ago | |
ATS | Rust | |
GNU General Public License v3.0 or later | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
ATS-Postiats
- What is the most feature-rich programming language
- Evolutie limbaje in industrie
-
The Little Typer – The Beauty of Dependent Type Systems, One Step at a Time
This is one of my two favorite books in The Little ...er series. The other is The Rational Schemer. These are two of the most advanced books in the series.
The Little Typer provides an introduction to dependent types. These can by used to guarantee things like "applying 'concat' to a list of length X and list of length Y returns a list of X+Y". It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Two interesting languages using dependent types are:
- Idris. This is basically "strict Haskell plus dependent types": https://www.idris-lang.org/)
- ATS. This is a complex systems-level language with dependent types: http://www.ats-lang.org/
The Rational Schemer shows how to build a Prolog-like logic language as a Scheme library. This is a very good introduction to logic programming and the implementation of backtracking and unification is fascinating.
This is an excellent series overall, but these two books are especially good for people who are interested in unusual programming language designs. I don't expect dependent types or logic programming to become widely-used in the next couple generations of mainstream languages, but they're still fascinating.
-
Does Rust have any design mistakes?
Not being ATS
-
The case against an alternative to C
> any safety checks put into the competing language will have a runtime cost, which often is unacceptable
This is completely wrong. The best counterexample is probably ATS http://www.ats-lang.org which is compatible with C, yet also features dependent types (allowing us to prove arbitrary statements about our programs, and check them at compile time) and linear type (allowing us to precisely track resource usage; similar to Rust)
A good example is http://ats-lang.sourceforge.net/DOCUMENT/ATS2CAIRO/HTML/c36.... which uses the Cairo graphics library, and ends with the following:
> It may seem that using cairo functions in ATS is nearly identical to using them in C (modulo syntatical difference). However, what happens at the level of typechecking in ATS is far more sophisticated than in C. In particular, linear types are assigned to cairo objects (such as contexts, surfaces, patterns, font faces, etc.) in ATS to allow them to be tracked statically, that is, at compile-time, preventing potential mismanagement of such objects. For instance, if the following line:
val () = cairo_surface_destroy (sf) // a type error if omitted
-
Security advisory: malicious crate rustdecimal | Rust Blog
For a low level language in which you actually need to prove that your code doesn't cause UB, see http://www.ats-lang.org/
-
Why is ATS not considered in the design of modern system languages?
Here's the homepage fo the language: http://www.ats-lang.org/. The trick to finding results about with google is to search "ATS programming language".
-
ESPOL, NEWP, Mesa, Cedar, Modula-2, Modula-2+, Modula-3, Oberon, Oberon-2, Component Pascal, Active Oberon, D, C#, F#, VB, Ada, Go, Swift, just a few examples.
In SPARK's case, you have to state your invariants in even greater precision than in Rust, and naturally it has worse inference. That's okay, the same happens in a certain language with Atrocious Type Syntax.
-
What are all the situations you can't do compile time type-checking when building a programming language?
Yes, things like mentioned in the post can be expressed and checked statically, as demonstrated by languages like Idris and ATS. ATS might be even more relevant as it's an imperative language too, it can get rather low-level (like talking about properties of C runtime functions) while proving required properties statically, and it includes a solver for certain amount of arithmetics so that you don't need to prove obvious mathematical identities to the compiler. http://www.ats-lang.org/
- Is it possible to make a functional programming language that is equivalent of Rust in terms of performance and resource efficiency?
wasmtime
-
Backdoor in upstream xz/liblzma leading to SSH server compromise
Just a documentation change, fortunately:
https://github.com/bytecodealliance/wasmtime/commits?author=...
They've submitted little documentation tweaks to other projects, too, for example:
https://learn.microsoft.com/en-us/cpp/overview/whats-new-cpp...
I don't know whether this is a formerly-legitimate open source contributor who went rogue, or a deep-cover persona spreading innocuous-looking documentation changes around to other projects as a smokescreen.
-
Unlocking the Power of WebAssembly
WebAssembly is extremely portable. WebAssembly runs on: all major web browsers, V8 runtimes like Node.js, and independent Wasm runtimes like Wasmtime, Lucet, and Wasmer.
-
Howto: WASM runtimes in Docker / Colima
cpu: 4 disk: 60 memory: 12 arch: host hostname: colima autoActivate: true forwardAgent: false # I only tested this with 'docker', not 'containerd': runtime: docker kubernetes: enabled: false version: v1.24.3+k3s1 k3sArgs: [] network: address: true dns: [] dnsHosts: host.docker.internal: host.lima.internal # Added: # - containerd-snapshotter: true (meaning containerd will be used for pulling images) docker: features: buildkit: true containerd-snapshotter: true vmType: vz rosetta: true mountType: virtiofs mountInotify: false cpuType: host # This provisioning script installs build dependencies, WasmEdge and builds the WASM runtime shims for containerd. # NOTE: this takes a LOOONG time! provision: - mode: system script: | [ -f /etc/docker/daemon.json ] && echo "Already provisioned!" && exit 0 echo "Installing system updates:" apt-get update -y apt-get upgrade -y echo "Installing WasmEdge and runwasi build dependencies:" # NOTE: packages curl, git and python3 already installed: apt-get install -y make gcc build-essential pkgconf libtool libsystemd-dev libprotobuf-c-dev libcap-dev libseccomp-dev libyajl-dev libgcrypt20-dev go-md2man autoconf automake criu pkg-config libdbus-glib-1-dev libelf-dev libclang-dev libzstd-dev protobuf-compiler apt-get clean -y - mode: user script: | [ -f /etc/docker/daemon.json ] && echo "Already provisioned!" && exit 0 # # Setting vars for this script: # # Which WASM runtimes to install (wasmedge, wasmtime and wasmer are supported): WASM_RUNTIMES="wasmedge wasmtime wasmer" # # Location of the containerd config file: CONTAINERD_CONFIG="/etc/containerd/config.toml" # # Target location for the WASM runtimes and containerd shims ($TARGET/bin and $TARGET/lib): TARGET="/usr/local" # # Install rustup: # echo "Installing rustup for building runwasi:" curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- --default-toolchain none -y source "$HOME/.cargo/env" # # Install selected WASM runtimes and containerd shims: # [[ -z "${WASM_RUNTIMES// /}" ]] && echo "No WASM runtimes selected - exiting!" && exit 0 git clone https://github.com/containerd/runwasi echo "Installing WASM runtimes and building containerd shims: ${WASM_RUNTIMES}:" sudo mkdir -p /etc/containerd/ containerd config default | sudo tee $CONTAINERD_CONFIG >/dev/null for runtimeName in $WASM_RUNTIMES; do case $runtimeName in wasmedge) echo "Installing WasmEdge:" curl -sSfL https://raw.githubusercontent.com/WasmEdge/WasmEdge/master/utils/install.sh | sudo bash -s -- -p $TARGET echo echo "`wasmedge -v` installed!" ;; wasmtime) echo "Installing wasmtime:" curl -sSfL https://wasmtime.dev/install.sh | bash sudo cp .wasmtime/bin/* ${TARGET}/bin/ rm -rf .wasmtime echo "`wasmtime -V` installed!" ;; wasmer) echo "Installing wasmer:" curl -sSfL https://get.wasmer.io | sh sudo cp .wasmer/bin/* ${TARGET}/bin/ sudo cp .wasmer/lib/* ${TARGET}/lib/ rm -rf .wasmer echo "`wasmer -V` installed!" ;; *) echo "ERROR: WASM runtime $runtimeName is not supported!" exit 1 ;; esac cd runwasi echo "Building containerd-shim-${runtimeName}:" cargo build -p containerd-shim-${runtimeName} --release echo "Installing containerd-shim-${runtimeName}-v1:" sudo install ./target/release/containerd-shim-${runtimeName}-v1 ${TARGET}/bin sudo ln -sf ${TARGET}/bin/containerd-shim-${runtimeName}-v1 ${TARGET}/bin/containerd-shim-${runtimeName}d-v1 sudo ln -sf ${TARGET}/bin/containerd-shim-${runtimeName}-v1 ${TARGET}/bin/containerd-${runtimeName}d echo "containerd-shim-${runtimeName} installed." cd .. echo "[plugins.\"io.containerd.grpc.v1.cri\".containerd.runtimes.${runtimeName}]" | sudo tee -a $CONTAINERD_CONFIG >/dev/null echo " runtime_type = \"io.containerd.${runtimeName}.v1\"" | sudo tee -a $CONTAINERD_CONFIG >/dev/null done echo "containerd WASM runtimes and shims installed." # # Restart the systemctl services to pick up the installed shims. # NOTE: We need to 'stop' docker because at this point the actual daemon.json config is not yet provisioned: # echo "Restarting/reloading docker/containerd services:" sudo systemctl daemon-reload sudo systemctl restart containerd sudo systemctl stop docker sshConfig: true mounts: [] env: {}
-
MotorOS: a Rust-first operating system for x64 VMs
When you say wasm container, you mean something like wasmtime that provides a non-browser wasm runtime?
https://github.com/bytecodealliance/wasmtime
-
Lightweight Containers With Docker and WebAssembly
We can't run this directly from the command line unless we install some runtime like wasmtime:
-
Prettier $20k Bounty was Claimed
The roadmap I linked above. The WASI folks have done a poor job at communicating, no doubt, but I'm surprised someone like yourself literally building a competitor spec isn't following what they are doing closely.
Just for you I did some googling: see here[0] for the current status of WASI threads overall, or here[1] and here[2] for what they are up to with WASI in general. In this PR[3] you can see they enabled threads (atomic instructions and shared memory, not thread creation) by default in wasmtime. And in this[4] repository you can see they are actively developing the thread creation API and have it as their #1 priority.
If folks want to use WASIX as a quick and dirty hack to compile existing programs, then by all means, have at it! I can see that being a technical win. Just know that your WASIX program isn't going to run natively in wasmtime (arguably the best WASM runtime today), nor will it run in browsers, because they're not going to expose WASIX - they're going to go with the standards instead. so far you're the only person I've met that thinks exposing POSIX fork() to WASM is a good idea, seemingly because it just lets you build existing apps 'without modification'.
Comical you accuse me of being polarizing, while pushing for your world with two competing WASI standards, two competing thread creation APIs, and a split WASM ecosystem overall.
[0] https://github.com/bytecodealliance/jco/issues/247#issuecomm...
[1] https://bytecodealliance.org/articles/wasmtime-and-cranelift...
[2] https://bytecodealliance.org/articles/webassembly-the-update...
[3] https://github.com/bytecodealliance/wasmtime/pull/7285
[4] https://github.com/WebAssembly/shared-everything-threads
-
Spin 2.0 – open-source tool for building and running WASM apps
Thanks for the question!
Spin could definitely run in more places than what we have pre-built binaries for. Specifically, we could run on all platforms Wasmtime supports today (https://github.com/bytecodealliance/wasmtime/releases/tag/v1...), including RISC and S390X, for example.
And while we have been experimenting a bit with running Spin on RISC, we haven't really had the bandwidth or requirement to build a production build for those yet.
Are you interested in a specific operating system or CPU architecture? Would love to understand your scenario.
-
Dave Cutler: The Secret History of Microsoft Windows [video]
> I used to think we'd eventually get to capability based security, but now I see we'll always be stuck with application permission flags, the almost worthless bastard cousin, instead.
My hope is that WASI will introduce capability based security to the mainstream on non-mobile computers [0] - it might just take some time for them to get it right. (And hopefully no half-baked status-quo-reinforcing regressive single—runtime-backed alternatives win in the meantime.)
[0]: https://github.com/bytecodealliance/wasmtime/blob/main/docs/...
-
Requiem for a Stringref
WasmTime finished finished the RFC for the implementation details in June: https://github.com/bytecodealliance/wasmtime/issues/5032
-
Should You Be Scared of Unix Signals?
[3]: https://github.com/bytecodealliance/wasmtime/pull/2611
What are some alternatives?
lean4 - Lean 4 programming language and theorem prover
wasmer - 🚀 The leading Wasm Runtime supporting WASIX, WASI and Emscripten
chapel - a Productive Parallel Programming Language
SSVM - WasmEdge is a lightweight, high-performance, and extensible WebAssembly runtime for cloud native, edge, and decentralized applications. It powers serverless apps, embedded functions, microservices, smart contracts, and IoT devices.
cicada - An old-school bash-like Unix shell written in Rust
quickjs-emscripten - Safely execute untrusted Javascript in your Javascript, and execute synchronous code that uses async functions
c3c - Compiler for the C3 language
wasm3 - 🚀 A fast WebAssembly interpreter and the most universal WASM runtime
virgil - A fast and lightweight native programming language
wasm-bindgen - Facilitating high-level interactions between Wasm modules and JavaScript
HVM - A massively parallel, optimal functional runtime in Rust
wasm-pack - 📦✨ your favorite rust -> wasm workflow tool!