4 ms·

I disagree. You're making two different arguments. The first is that PLT does not study suitability, but then you switch course and say that math analagously ca

by ouid 7y ago

I disagree. You're making two different arguments. The first is that PLT does not study suitability, but then you switch course and say that math analagously can define suitability for specific tasks but suitability is not (and this is my own words) a normed space. Programming language theory does not, in fact, make value judgments, but it does make statements upon which value judgments can be built given context, which contradicts your first statement.

pron 7y ago
I think you've misread my comment. Also, of course theory could be used to make judgment given all the necessary context, but the context, in this case, is much harder to obtain than the theory. If we knew whether a language's type system being sound is greatly positive (for some metric), slightly positive, neutral, slightly negative or greatly negative, then the knowledge that a certain language is sound or not could be valuable in making certain judgments. But PLT does not even attempt to ask that question, and it seems to be a much harder question than the ones PLT does ask. Don't get me wrong -- I think that PLT is a valuable theory, but people are often confused about what it actually studies. PLT most certainly cannot tell us whether certain language designs are desirable or not as that is not what the theory studies. It can't even tell us if certain language designs lead to more correct programs or programs that are easier to read. It does tell us that if certain typing rules are used, then, say, all types in the language can be inferred, or that a system with certain typing rules is sound.
- ragona 7y ago
  I’m new to this space so I’m not sure how PLT is distinct from formal verification, but my view of it is that formal methods are another form of testing. Unit testing also does not guarantee that you’re testing the right things, but it’s a good way to catch issues post-compile but pre-release. Formal verification moves that so that you catch issues as part of the compilation step, which is just another tool in the general toolbox of finding errors before you ship them to your users. It’s not about proving that your spec is good, it’s about automatically generating tests that find certain types of bugs.
  - pron 7y ago
    Formal methods are a large set of methods that allow you to analyze a program in ways that can verify it satisfies certain (correctness) properties. Most formal methods don't generate tests (although some do), but the term "compile-time" is not often used, as most formal methods are not part of the compiler. There is some overlap between PLT and formal methods, as that some concepts studied in PLT -- most notably type systems -- can be used for formal verification, but the main thrust of formal methods uses other techniques. Both disciplines heavily rely on formal logic.

by ouid 7y ago

pron 7y ago

I think you've misread my comment. Also, of course theory could be used to make judgment given all the necessary context, but the context, in this case, is much harder to obtain than the theory. If we knew whether a language's type system being sound is greatly positive (for some metric), slightly positive, neutral, slightly negative or greatly negative, then the knowledge that a certain language is sound or not could be valuable in making certain judgments. But PLT does not even attempt to ask that question, and it seems to be a much harder question than the ones PLT does ask. Don't get me wrong -- I think that PLT is a valuable theory, but people are often confused about what it actually studies. PLT most certainly cannot tell us whether certain language designs are desirable or not as that is not what the theory studies. It can't even tell us if certain language designs lead to more correct programs or programs that are easier to read. It does tell us that if certain typing rules are used, then, say, all types in the language can be inferred, or that a system with certain typing rules is sound.

ragona 7y ago
I’m new to this space so I’m not sure how PLT is distinct from formal verification, but my view of it is that formal methods are another form of testing. Unit testing also does not guarantee that you’re testing the right things, but it’s a good way to catch issues post-compile but pre-release. Formal verification moves that so that you catch issues as part of the compilation step, which is just another tool in the general toolbox of finding errors before you ship them to your users. It’s not about proving that your spec is good, it’s about automatically generating tests that find certain types of bugs.
- pron 7y ago
  Formal methods are a large set of methods that allow you to analyze a program in ways that can verify it satisfies certain (correctness) properties. Most formal methods don't generate tests (although some do), but the term "compile-time" is not often used, as most formal methods are not part of the compiler. There is some overlap between PLT and formal methods, as that some concepts studied in PLT -- most notably type systems -- can be used for formal verification, but the main thrust of formal methods uses other techniques. Both disciplines heavily rely on formal logic.