Comment by ashton314
2 years ago
I am going to be the token programming language researcher and say that what you really want is a dependently typed assembly language that your dependently typed higher level language lowers to. One school of thought that has yet to bear fruit in “mainstream“ programming, but gives tantalizing hints of what is possible, is expressing increasing amounts of your programs constraints in the type system, thereby informing the compiler precisely about your intent.
> 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).
1 reply →
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.