[AnthonBerg]

A dependently typed language is executed on a computer, therefore it is expressible in assembly code. Like sentences are expressed with words which are expressed with, say, letters. Letters are not sentences, but sentences do guide the expression of letters and vice versa. And sentences can indeed be made out of letters.

[anon291]

Neural networks are expressed and represented by mathematical symbols, yet those mathematical symbols alone cannot make a prediction or do anything useful.

No one is saying assembly language cannot be used to write a dependently typed language system, with a type checker and runtime (which are one and the same in a DT language anyway). However, that does not make assembly language dependently typed.

You are committing the logical error of assuming that the result of a process means inputs to the process are equal to the outputs. Just because I could take grain and make it into bread doesn't mean grain is equivalent to bread.

[deltaonenine]

When talking about these things there is a meta level we are targetting that you're not understanding. Types exist at a meta level and are part of the language.

Assembly language does not have types. What you can do is create a new language with assembly and have that language have types. The reason why it has to be done this way is because these types of checks CANNOT happen at runtime. It's a pre-runtime check that prevents the code from even running if it's not correct.

Think about it. Can you add types to assembly language without creating a new language? No.