4 ms·

One can look at the source code to a program, the libraries it uses, the compiler for the language, and the ISA spec for the machine language the compiler gener

One can look at the source code to a program, the libraries it uses, the compiler for the language, and the ISA spec for the machine language the compiler generates. You can know that there are no hidden unspecified quantities because programs can't work without being specified. When you get down to the microcode of the CPU that implements the ISA you might have an issue if it's ill-specified. You might be talking about an ISA like RISC-V, though, specified at a level sufficient to go down to the gates. You might be talking about an ISA like 6502 where the gate-level implementations have been reverse-engineered. You can take programming all the way down boolean logic if you need to and the tools are readily available. They don't rely on you "just knowing" something.

Jensson 5y ago
> One can look at the source code to a program, the libraries it uses, the compiler for the language, and the ISA spec for the machine language the compiler generates. You can know that there are no hidden unspecified quantities because programs can't work without being specified. I doubt you actually can do that and understand it all. A computer can do it, but I doubt you the human can do that and get a perfect picture of any non trivial program without making errors. Human math is a human language first and foremost, its grammar is human language which is used to define things and symbols. This lets us write things that humans can actually read and understand the entirety of, unlike a million lines of code or cpu instructions. Show me a program written by 10 programmers over 10 years and I doubt anyone really understands all of it. But we have mathematical fields that hundreds of mathematicians have written over centuries, and people still are able to understand it all perfectly. It is true that a computer can easily read a computer program, but since we are arguing about teaching humans you would need to show evidence that humans can actually read and understand complex code well.
pjc50 5y ago
> because programs can't work without being specified. Someone hasn't read the C spec, with all its specified as undefined behavior. Programs working on real systems is very different from those systems being formally specified. I suspect that if you only had access to the pile of documentation and no real computer system - if you were an alien trying to reconstruct it, for example - you'd hit serious problems.
- throwaway31338 5y ago
  Undefined behavior isn't a feature. A spec isn't an implementation, either. All behavior in an implementation can be teased-out if given sufficient time. > if you were an alien trying to reconstruct it, for example - you'd hit serious problems. I can't speak to alien minds. Considering the feats of reverse-engineering I've seen in the IT world (software security, semiconductor reverse-engineering) or cryptography (the breaking the Japanese Purple cipher in WWII, for example) I think it's safe to say humans are really, really good at reverse-engineering other human-created systems from close-to-nothing. Starting with documentation would be a step-up.
  - Jensson 5y ago
    > All behavior in an implementation can be teased-out if given sufficient time. Can it? Given what? You would need to understand how the CPU is supposed to execute the compiled code to do that. In order to understand the CPU you would need to read the manual for its instruction set, which is written in human language and hence not any better defined than math. At best you get the same level of strictness as math. If you assume you already have a perfect knowledge of the CPU workings, then I can just assume that you already have perfect knowledge of the relevant math topic and hence don't even need to read the paper to understand the paper. Human knowledge needs to come from somewhere. If you can read a programming language manual then you can read math. Every math paper is its own DSL in this context with its own small explanations for how it does things.
    - webmaven 5y ago
      > Every math paper is its own DSL in this context with its own small explanations for how it does things. That's really the point though: not every piece of software defines it's own DSL, nor does it necessarily incorporate a DSL from some library or framework (which in turn may or may not borrow from other DSLs, etc.). It is also impossible to incorporate something from other software without actually referencing it explicitly. Math, though, is more like prose in this respect – while any given novel probably has a lot of structure, terminology, and notation in common with other works in its genre, unless it is extremely derivative it almost certainly has a few quirks and innovations specific to the author or even unique to that particular work that you can absorb while reading or puzzle out due to context, as long as you accept that the context is quite a lot of other works in the genre (this is more true of some genres/subfields than others). Unlike novels, at least in math papers (but not necessarily books) you get explicit references to the other works that the author considered most relevant, but those references are not usually sufficient on their own, nor necessarily complete, and you have to do more spelunking or happen to have done it already. Finally, like prose, with math you have to rely on other (subsequent) sources to point out deficiencies in the work, or figure them out on your own. Math papers, once published, don't usually get bug fixes and new releases, you're expected to be aware (from the context that has grown around the paper post-publication) what the problems are. Which means reading citations forward in time as well as backward for each referenced paper. The combinatorial explosion is ridiculous. It would be great if there were something like tour guides published that just marked out the branching garden paths of concepts and notation borrowed and adapted between publications, but textbooks tend to focus on teaching one particular garden path.

Jensson 5y ago

> One can look at the source code to a program, the libraries it uses, the compiler for the language, and the ISA spec for the machine language the compiler generates. You can know that there are no hidden unspecified quantities because programs can't work without being specified. I doubt you actually can do that and understand it all. A computer can do it, but I doubt you the human can do that and get a perfect picture of any non trivial program without making errors. Human math is a human language first and foremost, its grammar is human language which is used to define things and symbols. This lets us write things that humans can actually read and understand the entirety of, unlike a million lines of code or cpu instructions. Show me a program written by 10 programmers over 10 years and I doubt anyone really understands all of it. But we have mathematical fields that hundreds of mathematicians have written over centuries, and people still are able to understand it all perfectly. It is true that a computer can easily read a computer program, but since we are arguing about teaching humans you would need to show evidence that humans can actually read and understand complex code well.

pjc50 5y ago

> because programs can't work without being specified. Someone hasn't read the C spec, with all its specified as undefined behavior. Programs working on real systems is very different from those systems being formally specified. I suspect that if you only had access to the pile of documentation and no real computer system - if you were an alien trying to reconstruct it, for example - you'd hit serious problems.

throwaway31338 5y ago
Undefined behavior isn't a feature. A spec isn't an implementation, either. All behavior in an implementation can be teased-out if given sufficient time. > if you were an alien trying to reconstruct it, for example - you'd hit serious problems. I can't speak to alien minds. Considering the feats of reverse-engineering I've seen in the IT world (software security, semiconductor reverse-engineering) or cryptography (the breaking the Japanese Purple cipher in WWII, for example) I think it's safe to say humans are really, really good at reverse-engineering other human-created systems from close-to-nothing. Starting with documentation would be a step-up.
- Jensson 5y ago
  > All behavior in an implementation can be teased-out if given sufficient time. Can it? Given what? You would need to understand how the CPU is supposed to execute the compiled code to do that. In order to understand the CPU you would need to read the manual for its instruction set, which is written in human language and hence not any better defined than math. At best you get the same level of strictness as math. If you assume you already have a perfect knowledge of the CPU workings, then I can just assume that you already have perfect knowledge of the relevant math topic and hence don't even need to read the paper to understand the paper. Human knowledge needs to come from somewhere. If you can read a programming language manual then you can read math. Every math paper is its own DSL in this context with its own small explanations for how it does things.
  - webmaven 5y ago
    > Every math paper is its own DSL in this context with its own small explanations for how it does things. That's really the point though: not every piece of software defines it's own DSL, nor does it necessarily incorporate a DSL from some library or framework (which in turn may or may not borrow from other DSLs, etc.). It is also impossible to incorporate something from other software without actually referencing it explicitly. Math, though, is more like prose in this respect – while any given novel probably has a lot of structure, terminology, and notation in common with other works in its genre, unless it is extremely derivative it almost certainly has a few quirks and innovations specific to the author or even unique to that particular work that you can absorb while reading or puzzle out due to context, as long as you accept that the context is quite a lot of other works in the genre (this is more true of some genres/subfields than others). Unlike novels, at least in math papers (but not necessarily books) you get explicit references to the other works that the author considered most relevant, but those references are not usually sufficient on their own, nor necessarily complete, and you have to do more spelunking or happen to have done it already. Finally, like prose, with math you have to rely on other (subsequent) sources to point out deficiencies in the work, or figure them out on your own. Math papers, once published, don't usually get bug fixes and new releases, you're expected to be aware (from the context that has grown around the paper post-publication) what the problems are. Which means reading citations forward in time as well as backward for each referenced paper. The combinatorial explosion is ridiculous. It would be great if there were something like tour guides published that just marked out the branching garden paths of concepts and notation borrowed and adapted between publications, but textbooks tend to focus on teaching one particular garden path.