Comment by almostgotcaught
2 years ago
> want is a dependently typed assembly language
Doesn't make any sense. The "type constraints" on assembly operands (registers and numbers) is the ISA and thus those constraints are combinatorial not logical
2 years ago
> want is a dependently typed assembly language
Doesn't make any sense. The "type constraints" on assembly operands (registers and numbers) is the ISA and thus those constraints are combinatorial not logical
You misunderstand. If I, at the assembly level, could express things like "this register ranges from 0 to 4"—I might be able to provide ever-lower levels of the stack with more information about my intent. Maybe the ISA can now do something clever to further optimize my program. Now, there will likely always be a time when all types are erased, but if we can push that erasure lower and lower in the stack, then compilers have more and more information about what we actually want them to do, provided our type systems are rich enough to express that intent.
> "this register ranges from 0 to 4"
that's not a type system, that's an ILP. and we already have that in many compilers (bindings to ILP solvers).
> Maybe the ISA can now do something clever to further optimize my program.
this is a malformed sentence - the ISA is fixed and isn't making any gametime decisions about your code (modulo branch prediction/cache-fretching). it's all in the compiler and like i said we already have this in many many compilers and it's surfaced in various ways (eg trip count on loops).
Those who say it cannot be done should not interrupt someone doing it.
https://www.cs.cmu.edu/~rwh/papers/dtal/OGI-CSE-99-008.pdf
It's not perfect, but dependently typed assembly languages isn't something I just made up. Maybe there's a mismatch between the terms we're using?
There's the reason "token programming language researchers" are incapable of understanding modern computer architectures: a huge gap where would have been EE education.
Correct - most of them think the goal is an infinite tower of sophisticated "abstractions" not realizing there's nothing abstract about a finite piece of silicon.