Conversation

One of my life dreams is still to build a computer from scratch, then also all of the software on it: the operating system, every language and compiler, and so on

123

Brendan Zabarauskas

@brendanzab

Jan 9

Been very interested in the stuff from assembly-upwards. I'd love to figure out how quickly you could get up to a workable type theory from a minimal foundation. - justine.lol/sectorlisp2/ - wiki.xxiivv.com/site/uxntal.ht - wiki.xxiivv.com/site/uxn_devlo - collapseos.org

Replying to

and

Also fun is microsoft.com/en-us/research - Also curious about typed assemblers too - and how hard they might be to build. It's all really interesting yet kind of intimidating at the same time!

microsoft.com

Coq: The world's best macro assembler? - Microsoft Research

We describe a Coq formalization of a subset of the x86 architecture. One emphasis of the model is brevity: using dependent types, type classes and notation we give the x86 semantics a makeover that...

8:30 AM · Jan 9, 2022Twitter Web App

Replying to

and

RISCV has a cool formal specification (you might alsready be aware of it though):

github.com

GitHub - riscv/sail-riscv: Sail RISC-V model

Sail RISC-V model. Contribute to riscv/sail-riscv development by creating an account on GitHub.

Replying to

and

Typed assembly language work I’m familiar with is from the 90s and is/was about giving you a runtime checkable proof that was sound with respect to original source language type safety. Eg has the right structures To compile closure representations to.