4 ms·

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 type

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.

almostgotcaught 2y 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
- tucnak 2y ago
  There's the reason "token programming language researchers" are incapable of understanding modern computer architectures: a huge gap where would have been EE education.
  - almostgotcaught 2y ago
    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.
- ashton314 2y ago
  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.
  - almostgotcaught 2y ago
    > "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).
    - ashton314 2y ago
      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 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?

almostgotcaught 2y 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

tucnak 2y ago
There's the reason "token programming language researchers" are incapable of understanding modern computer architectures: a huge gap where would have been EE education.
- almostgotcaught 2y ago
  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.
ashton314 2y ago
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.
- almostgotcaught 2y ago
  > "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).
  - ashton314 2y ago
    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 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?