fmap

5 ms·

31.
by fmap 8y ago
Slightly tongue in cheek, but the analogy to programming is this: > "Almost everything most programmers do can be done both in x86 assembly and your favorite non-kooky programming language. Certain Powers That Be seem to have decide
32.
by fmap 8y ago
> Everything in mathematics is divorced from reality. Mathematics is an abstraction, but it is still useful for talking about concrete problems. Your mathematical assumptions can be either close or far away from your problem domain. Some
33.
by fmap 8y ago
> “I never really thought about it, but it doesn’t much affect my work day to day one way or the other” In my experience, people won't come out and say it, but this seems to be what everyone is thinking. :) The problem with this is
34.
by fmap 8y ago
You're right. Classical measure theory lives in a model divorced from physical reality. You can show that all of the fancy counterexamples which necessitate the complicated constructions of measure theory are artificial (e.g., the char
35.
by fmap 8y ago
I'm referring to the axiom that being godlike is a positive property. You can show that being godlike is a positive property iff god exists.
36.
by fmap 8y ago
You may be right that it is common to dismiss arguments that invoke Gödel's theorem. I've been guilty of this myself. However, just like with quantum mechanics the reason is that there are just so many people who invoke Gödel&#x27
37.
by fmap 8y ago
There is actually a neat way around this by using typed assembly language/proof carrying code. If you had a type preserving compiler down to machine code you could use a separate proof checker (which you presumably wrote by hand in mac
38.
by fmap 8y ago
It's not misleading in this case. It's used in practice. You have to understand that CompCert's main competition in this space was an ancient version of GCC without any optimizations. This is mostly an issue of certificatio
39.
by fmap 8y ago
There's a separate project that solves this problem (CertiCoq https://www.cs.princeton.edu/~appel/certicoq/ ). It's making progress, but these things take time. :)
40.
by fmap 8y ago
Textbooks are usually supposed to be accessible to a wide audience so it makes sense when discussing foundations to start from a (hopefully) familiar set theory. It's usually a trade-off, since you end up repeating yourself when it com
41.
by fmap 8y ago
> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification I suspect that most bugs are introduced because programmers do not have a clear idea of what their code is supposed to
42.
by fmap 8y ago
> So what exactly is the standard we are working to? Is proof reasonably superior to more effort testing? Empirically, yes it is (see e.g. "Finding and understanding bugs in C compilers"). Testing can show the presence of bugs,
43.
by fmap 8y ago
> All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic What gave you thi
44.
by fmap 8y ago
Elm is different to ML in that it is explicitly designed to be a pure language. Purity is important for the Elm architecture and allowing arbitrary side effects in your apps would break everything. That said, you could add effects and a Jav
45.
by fmap 8y ago
That's amazing! Do you have any insight as to which structural properties make this problem simple? The reason I was asking after tree-width is that control and dataflow graphs in structured programming languages usually have small tre
46.
by fmap 8y ago
Ok, my first reaction is that this is that it's really wonderful work - straightforward and with a big payoff at the end. But this really begs the question: why hasn't this been done before? People have been throwing resources at
47.
by fmap 8y ago
The article is underselling Erlang's meteoric success. "Adoption was slow during the first few years." - After 5 years there was an international conference devoted to Erlang, a global community around it and the language enj
48.
by fmap 8y ago
He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. In general, you can do this exhaustive search with any "compact" type and there a
49.
by fmap 8y ago
That was a poor choice of words. Models of lambda calculus are invariant under beta-eta conversion, which is what I meant by program equivalence, but which is not the same thing as contextual equivalence. Thus you get a representation invar
50.
by fmap 8y ago
Most examples I tried didn't work very well, but when it did work it was truly neat. The performance makes sense from a quick glance into the paper. The model represents programs as paths in the AST, which is not sufficient to reconstr
51.
by fmap 8y ago
> it is common because academia loves OOP. Absolutely not! I doubt that anybody was ever taught OOP in an academic PL course, unless it was really an "introduction to programming" course, or their professor was working on this
52.
by fmap 8y ago
This is a really wonderful paper. For several years now we have been teaching a seminar about functional programming every year, where students present functional pearls (for the most part). This paper has been a staple of the seminar and I
53.
by fmap 8y ago
> When possible errors are part of the function specification, on the other hand, we are almost OK. This is the single best piece of advice in this article. The second thing you have to document is the postcondition in case of an error -
54.
by fmap 8y ago
> does "differentiation" have any applications in implementing more complete programming languages? I'm not sure about implementing per se, but you can extend some notion of differentiation to richer programming languages:
55.
by fmap 8y ago
These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.
56.
by fmap 8y ago
I am not sure what the parent meant specifically, but yes, there is quite a lot of work on quantum physics and logic, with regular conferences ( https://arxiv.org/html/1701.00242 ) and some truly fascinating models for i
57.
by fmap 8y ago
Lie groups come up very naturally in synthetic differential geometry (SDG) ( http://www.fuw.edu.pl/~kostecki/sdg.pdf ). In fact, the main advantage of SDG over the classical formulation of differential geometry is that i
58.
by fmap 8y ago
You have far more freedom in modeling intuitionistic logic than you think. :) In this case, the point is that in a logic for cryptography, you would have a type "S" of "bit strings of arbitrary but unknown length" which
59.
by fmap 8y ago
That's a nice way of introducing type state programming in an affine programming language! In general though, type state programming would be even nicer in a linear language. For example, in the http server I could start writing a resp
60.
by fmap 8y ago
Let me just stress the first point, because that's exactly where Rust and C++ differ: C++ templates really are untyped . There is no way to check whether a template definition is correct. A C++ compiler has to first expand the templat

More ›