fmap

14 ms·

181.
by fmap 10y ago
There are two problems in interactive theorem proving. The first is proving theorems, which is essentially tree search and should actually be amenable to Monte-Carlo tree search. Based on my own experiences, it seems reasonable that this st
182.
by fmap 10y ago
What exactly are you arguing for? Closures can be implemented using closure conversion as a derived form in most languages. That's how you compile the code in the first place... The point is that you reason about closures as ordinary f
183.
by fmap 10y ago
The environment contains references/copies/borrows of local variables, depending on a number of conditions on the code. Since the environment struct is generated by the compiler, this is different from a method call where you spec
184.
by fmap 10y ago
It depends. There are some topics for which the historical context provides the perfect motivation. Which problems were considered important and why? How does this theory solve these concrete problems? It is much easier to motivate students
185.
by fmap 10y ago
I'm not the OP, but higher-order functions in Rust are a leaky abstraction. Internally, functions are implemented as closures which might capture ownership and potentially duplicate/destroy variables in their scope. This means tha
186.
by fmap 10y ago
> The programming language theory community indeed tries to make mathematical reasoning explicit, but they're trying to make reasoning possible within the construction language (like the algebra of gears). We discussed this point be
187.
by fmap 10y ago
Barendregt, in his famous book on the lambda calculus has a great justification: once you look at models for the lambda calculus you are forced to introduce notions from analysis, such as continuity. The arguments and proofs would feel righ
188.
by fmap 10y ago
> They already have to handle the node disappearing. The only difference is that you can sever the connection from particular handles via the process containing the node/socket, if it chooses to. Otherwise, there is no difference. L
189.
by fmap 10y ago
Judging by this description, Bus1 sounds very much like an object capability system. There is a lot of theoretical and practical evidence that this is a good programming model, and as far as I know it does not currently exist in linux. Mayb
190.
by fmap 10y ago
I think there are different discussion forums for different things. Right here, I'm talking to you because I'm interested in hearing your point of view and perspective, and I want to know how you react to mine. In a professional c
191.
by fmap 10y ago
> Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation Maybe he said something like "[...] can all be seen as abstract interpretations". But it's probably not always usefu
192.
by fmap 10y ago
> Abstract interpretation has to do with every proof technique regarding computation. Are we talking about the same thing? Abstract interpretation as formulated by Cousot consisting of a covariant galois connection between a particular k
193.
by fmap 10y ago
> Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties. Abstract interpretation has nothing to do with disjunctive well-found
194.
by fmap 10y ago
> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. You are seriously overselling these results. Here's one way to make termination proofs modu
195.
by fmap 10y ago
> There are various results showing that the difference in size between an informal proof (even when correct, which, as experience shows often isn't[1]) and a formal one may be exponential. What's the definition of an informal
196.
by fmap 10y ago
You might be interested in reflection/implicit configurations: https://hackage.haskell.org/package/reflection This (ab)uses Haskell's type class mechanism to essentially implement dependency injection directl
197.
by fmap 10y ago
This is very interesting work! Do you have axiomatic semantics for Ivory and Tower, and/or specifications for SMACCMPilot? If so, it might be interesting to show specification preservation from Ivory to the Verified Software Toolchain
198.
by fmap 10y ago
Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall functions, with uncomputable property foo, we have bar". Plenty of
199.
by fmap 10y ago
Defining what a pure function in JavaScript is seems to be the difficult problem here. Maybe we should call a function pure if "given identical, pure arguments, it returns identical, pure results". You would also need to def
200.
by fmap 10y ago
So by now I've actually read the (abridged) paper and skimmed the full paper. And the paper has nothing to do with consistency problems, since they only consider boolean propositional logic... Assigning consistent probabilities in the
201.
by fmap 10y ago
Peano arithmetic, as in classical first-order logic with the peano axioms is a small subsystem of MLTT with natural numbers and no universes. If you come from a set theory background, then universes are really akin to Grothendieck universes
202.
by fmap 10y ago
> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with L
203.
by fmap 10y ago
The infinity groupoid models of type theory have already revolutionized our understanding of equality in type theory. So far, the 21st century has been an incredible time for logicians. There are also older, and very different topological m
204.
by fmap 10y ago
Are you sure about that? First, many higher-order constructs boil down to simple first-order control flow after partial evaluation (see e.g. AnyDSL https://anydsl.github.io/#publications ). Inferring stack size bounds in the
205.
by fmap 10y ago
The article is spot on. Even the proposed construction of a category by taking the quotient of closed terms under observational equivalence probably wouldn't really work. You may be able to get a category this way, but it just wouldn&#
206.
by fmap 10y ago
Yeah, I don't think we actually disagree here... all I was saying is that there are proofs which are genuinely non-constructive, and this isn't one. You are arguing that this usage of "constructive" is basically meaningl
207.
by fmap 10y ago
Any proof using an instance of excluded middle or choice which is not constructively valid. For example, see the first proof on this page: http://www.cut-the-knot.org/do_you_know/irrat.shtml
208.
by fmap 10y ago
For the vast majority of proofs you are exactly right. There are some exceptions, though, since you don't necessarily have a choice principle, even under a double negation translation. This is why you need Markov's priniciple in a
209.
by fmap 10y ago
It's a bit more subtle than that. Operationally, the proof will end up being exhaustive search, but you also need a constructive termination proof. This is not a very helpful way to think about these things though. What I meant is that
210.
by fmap 10y ago
Yes, this is a good idea. What I'm concerned about is that there is no standard terminology. The paper - and another comment in here! - is talking about the proof being "non-constructive", when in reality it is a constructive

More ›