= 27d567bc2d48d9f40e9ccc20ea370b15)
Kawoomba comments on Course recommendations for Friendliness researchers - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (113)
How is the distinction between functional and imperative programming languages "not a real one"? I suppose you mean that there's a continuum of language designs between purely functional and purely imperative. And I've seen people argue that you can program functionally in python or emulate imperative programming in Haskell. Sure. That's all true. It doesn't change the fact that functional-style programming is manifestly more machine checkable in the average (and best) case.
Agreed. The most poorly programmed functional programs will be harder to machine check than the mostly skillfully designed imperative programs. But I think for typical programming scenarios or best case scenarios, functional-style programming makes it hands-down more natural to write the correct kind of structures that can be reliably machine checked and imperative programming languages just don't.
The entry level functional programming course is going to focus on all the right things: type theory, model theory, deep structure. The first imperative programming course at most universities is going to teach you how to leverage side-effects, leverage side-effects more, and generally design your code in a way that makes it less tractable for verification and validation later on.
Pretty much by definition all (Turing-complete) programming languages can in principle be transformed into each other, it's not even very hard: just take the ASM code and build some rudimentary reverse compiler that creates some strange looking code in your desired goal language.
For practical purposes, machine checkability is easier for functional languages, but it's a difference in degree, not one in kind. (Corrections welcome!)
The code wouldn't just look strange, it would likely be more complex than code written directly in the language using its standard style at a high level to solve the same problem. The reversed compiled code would be harder to analyze, and harder to know what would be useful to prove about it, than code written directly in the target language with the reasoning behind why the programmer expects it to work serving as a guide to construct the proof.
Yes, however from what I recall about such proving methods, they were quite formulaic and about an equal amount of pain for each line (I should dig out some references some time), so the difference may not be as pronounced. Be that as it may, I agree that there is a difference in degree, which does matter for practical purposes.
I expect it is more than a difference in degree. When the programmer can tell the automated theorem prover that the return value of a certain function always satisfies some condition that other functions rely on, the theorem prover can try to prove that condition holds and use that fact for other proofs without being distracted by other possible conditions that are not relevant. This makes the search space much smaller.
The point is that the programmer having some understanding of the proof checker, and designing the code to be not just correct, but provably correct in a reasonable amount of time makes a big difference from the general problem of proving things about arbitrary code where you run into the halting problem.
I agree with both your example ("making the search space much smaller") and your explanation ("makes a big difference"), we just differ on whether thus changing the resource requirements constitutes a change in kind, or one in degree.
Also, I took your "code would likely be more complex" as "be less human-understandable", as opposed to its actual Kolmogorov complexity, which afaik would be identical.