l_dopa
> The notation g ∘ f is read as "g of f "...
If you're talking about ML-style modules, that really can't be farther from the truth, both in theory and how they're used in practice.
Modules can be used (among many other things) to implement abstract data types, which are conceptually a bit easier to compare to objects[0]. Then you'd have to go into structural vs nominal typing, functors vs generics, etc.
[0]https://www.cs.utexas.edu/users/wcook/papers/OOPvsADT/CookOO...
I think it's the particular combination of only having nominal typing, only allowing the oo-flavor of data abstraction, and encouraging programming with state and using inheritance for code reuse that leads to the object-spaghetti nonsense in heavily-oo Java/C++ codebases.
Another big one is that module types are structural: you don't have to declare all the module types implemented by a module when you define the module.
Sorry, I may have read that into your comment.
> the code itself needs to be pure
But that's also incorrect. Just because you can't replace an effectful computation with a value doesn't mean you can't reason equationally. You can also have benign effects that are unobservable, for example, memoization.
> Not sure how to parse that
I meant that functions with effects are just functions with computation type at the meta level. I.e. there's nothing more "mathematical" about only allowing nontermination in your language. It's just the simplest case.
The fact that your grand ideas about machine and language models doesn't apply to the lambda calculus should be a hint. We know how lambda calculus relates to typed languages: it's a degenerate case with a single type. Any differences in the complexity of type-inference or checking are between language models. You can't (without wildly waving your hands) formulate a meaningfully comparable problem for TM states.
It's also unclear if you're talking about the complexity of type inference or type checking, what annotations you're allowing, etc. Your claims about complexity re: states of typed languages are too hand-wavy to engage with.
And yet there's still a glaring error: for a very popular machine model, namely the C abstract machine, it's undecidable whether a state is meaningful (regardless of how you set up your parsing problem).
So, you have an interesting idea about the difference between machine models and languages but it clearly doesn't hold together. People have been studying the relationship between machine models and languages for quite some time, and it's relatively well understood. Machine models are one of the many ways to give semantics to languages. They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.
Languages are not so much a collection of features ...
Calling them just domain specific ...
Again, I'm just asking: why mess with the basics? Why require encoding simple, universal concepts in terms of an ad-hoc object system? You can still have an object system on top, if you find that helps with the really complicated cases, but why encode the parts of your code that are simple in terms of much more complicated, derived concepts?
Why should expressing something basic like a tagged union require a detour through the quirks of a particular object system? Ditto for polymorphism, modularity, etc, etc. Clearly we disagree on how useful objects really are in practice, fine. Why not add these domain-specific features on top of a core language with simple semantics? It worked fine for lisps. Luckily, after a couple of decades of "everything is an object!" nonsense, that seems to be where newer languages (Rust, Swift) are headed.
The simplest case is replacing an expression with its value, given an environment of lexical bindings that are apprent from the source program. Not much investigation necessary. That's FP.
For OO code, you just need to keep track of a lot more context: the state of the receiver of the currently executing method, its heirarchy of parent classes, the runtime class of each object because late binding is pervasive. Of course you can write code that doesn't use any OO features, but the languages clearly aren't designed for it. See: any number of "functional C++" articles.
And, of course, you can get the same kind of highly dynamic behavior in FP languages by explicitly using open recursion, higher-order state and hiding everything behind existentials. But very few codebases do that because the vast, vast majority of the time just one of these features is enough to solve a problem.
Whether or not you want your language to enforce segregating (most) effects is a separate issue, about which reasonable people can disagree.
Really understanding where FP is coming from requires an introduction to programming language semantics[1]. Interesting stuff, but not immediately useful to a working C programmer.
[0] https://existentialtype.wordpress.com/2011/03/15/boolean-bli...
My point was not something about manipulating weights directly vs. augmenting the training set. The analogy is roughly, find a misclassification : add particular input to training set :: find a bug : add a patch/test case. I'm playing devil's advocate, of course, and there are obvious, important differences.
> The difference is that all human written systems was once understood by a human
But that's not one of them! In practice, we create software systems by getting some rough intuition about an interface, wiring together some components, then checking the results empirically. Basic components that everything else is built on, C compilers for instance, are based on ambiguous, even contradictory specifications.
In both cases we can only fix a particular instance of an error and effectively have no way to show that similar errors don't exist, or even that we didn't introduce new bugs with the fix.
I think that supports the article's point that C++, Java, etc. only support certain language features in an ad-hoc way tied to their object systems, making them, among other things, poor teaching languages.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.3...
> The truth is that Haskell -- like all programming language -- has made a design choice, which was to bake in correctness proofs based on the Curry-Howard correspondence into the language
Haskell is not a logic and is not used to write proofs for program verification. General-purpose functional languages don't have all that much to do with CH, and they don't include any design decisions that favors a particular approach to verification. The type system helps you enforce useful invariants in your code and can make verification easier, but it's completely orthogonal to how you can prove programs correct.
> I think C-H has so far disappointed, because 1., people don't seem to want it, and 2. because other verification systems (like KeY) or the verifiable imperative, reactive real-time languages of the eighties (like Esterel) whose descendants are still in use today, have so far been used to much better effect.
Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification. So, different tools for a different purpose. Having said that, they have proven to be very useful for verification of complex systems like those you listed, where existing tools have trouble even stating what correctness means. That is, they can help us answer the question "how can we be certain that this compiler, verification system, etc. is correct?" That typically includes representing your object language in your theorem prover and proving things about the language, which is quite different than showing that an algorithm meets some specification.
> But the notion of subset => simpler is a mathematical notion with no relevance to cognition. If humans operated in this way, natural languages would have been much more mathematically simpler, too.
You can show that, quite literally, any "true property" of a program in your more complicated language is also true of the corresponding program in your simpler language. So, if you come to some correct conclusion, even if the way you reason is completely bogus and just happens to work, it will be valid for your simpler language.
There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans". That's not to say that the current crop of functional languages is presented in the easiest way for people to understand, but that's an entirely different problem independent of semantic considerations.
[1] https://www.reddit.com/r/programming/comments/3i1l9n/from_im...
Something like http://vst.cs.princeton.edu/ has a much, much stronger case for enabling "100% correct software".
The field that gave rise to FP has a lot to say about how we specify languages and their properties and how we prove things about programs in general. That includes languages with all kinds of effects: state, exceptions, concurrency, etc, and equally as imporant, mechanisms for abstraction and modularity. There's currently no other "foundation" for computation that lets us define these ideas formally.
In discussions of FP, the contributions of the field get reduced to "programming with functions".
My point was that it's possible to systematically extend (or restrict) the lambda calculus and associated techniques. You can add effectful operations and give them semantics (e.g. as functions on stores), define a cost semantics and prove whatever you want while being completely formal.
Try extending RAMs with dynamic allocation, call stacks, or anything to make it more natural to write down a whole algorithm. Try proving something about the composition of RAM programs. I don't think you'll get very far.
http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis
> A better "foundation" would try to describe computational behavior and reason about it, instead of abstracting it away
A lot of interesting research does exactly this, and a lot of it has found its way into ML-family languages. The starting point (or "foundation") in every case is a typed lambda calculus. Machine models, like turing machines, are just annoying to reason about and not extensible in any meaningful way.
Could you expand on this? Based on the problem statement page, this seems to be the exact problem MLRISC tried to address. Is there something that keeps it from working well in practice?