hoping1

9 ms·

31.
by hoping1 3y ago
I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages. Typechecking stack-
32.
Advanced Typechecking for Stack-Based Bytecode(ryanbrewer.dev)
1 points by hoping1 3y ago|1 comments
33.
by hoping1 3y ago
I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages
34.
A Beginner's Guide to Programming Language Academia(ryanbrewer.dev)
3 points by hoping1 3y ago|1 comments
35.
by hoping1 3y ago
I wrote a post cataloguing my experience reading papers on programming language things. These are things I wish I'd been aware of when I just started out; I hope this can make the ivory tower of PL theory a little more accessible to ot
36.
by hoping1 3y ago
In this post I talk about Crary et al.'s Calculus of Capabilities, how it can be used for safe manual memory management without requiring values be used linearly in any way, and why I chose it for SaberVM.
37.
Safe Manual Memory Management with Coeffects(ryanbrewer.dev)
3 points by hoping1 3y ago|1 comments
38.
by hoping1 3y ago
Just realized I misspelled Karl Crary's last name! It should be Crary, not Krary. Embarrassing!
39.
by hoping1 3y ago
Mostly right. We're still in a prototyping phase for sure. The verifier is still in progress, the execution will follow. That said, the main method of the program reads from a file called `bin.svm` which has the bytecode, and which cou
40.
by hoping1 3y ago
Yeah there are a number of successful compilers from functional languages to Wasm. It's definitely doable. I just wanted a backend that was more focused on being a portable target for functional languages. Throughout these comments I l
41.
by hoping1 3y ago
Wasm has a lot of great proposals that excite me but has other disqualifying factors for me. I don't want to be required to use garbage collector, I'm concerned about how much Wasm is growing in scope with all the proposals, I&#x2
42.
by hoping1 3y ago
That's true, mostly because of the JVM's garbage collection. SaberVM also hopes to be a good way to run untrusted code, like the JVM, but it can run much lower level, higher performance code safely, using arenas and the theory pow
43.
by hoping1 3y ago
The type system is stolen from some of the work on TAL (typed assembly language), by Greg Morrisett and others. In my implementation at the moment it's linear first in the size of the program and then there's a little more checkin
44.
by hoping1 3y ago
Totally! It's a really exciting time to be in langdev.
45.
by hoping1 3y ago
Definitely not ready for that just yet. I've just started making the project public, it's still a little far from a usable state. I love the energy though! I'll post about my progress along the way.
46.
by hoping1 3y ago
Yeah I wrote that targeting a more langdev audience, to be fair. Those are great questions! There’s a lot to answer there so unfortunately my answer is a bit long, I hope that’s ok. 1) Why have regions in the VM instead of compilers that ta
47.
SaberVM(ryanbrewer.dev)
135 points by hoping1 3y ago|18 comments
48.
by hoping1 3y ago
In this post I announce a new abstract machine oriented towards executing functional languages in a memory-safe and portable way.
49.
by hoping1 3y ago
Implicit products are a fascinating approach to universal quantification in dependent type theory, as well as proof irrelevance/erasure in compiler implementation. I wrote this post to bring some awareness to a really cool idea. It is