mafribe

33 ms·

271.
by mafribe 10y ago
If you use ¬¬ϕ = ϕ in your proof, you loose constructivity. Why would you care about this? Simplifying a bit, in a constructive proof, every existential statement ∃x.ϕ comes with a witness c such that ϕ is true when x is replaced by c. Li
272.
by mafribe 10y ago
A good proxy measure for the accuracy of BBdM's prediction would be how rich he got out of them. Given that BBdM's mostly concerned with macroscopic predictions about politics his claim [1] that he was right in 2/3 of his pre
273.
by mafribe 10y ago
I'd be interested in your (brief if you have not time) suggestions what kind of novel interfaces you have in mind. I have spent too much time on the command line to have any creative thoughts about radically different interfaces for ve
274.
by mafribe 10y ago
Maybe I'm particularly easy to make happy. Compilers, in particular optimising compilers are notoriously buggy, see John Regehr's blog. An old dream was to verify them. The great Robin Milner, who pioneered formal verification (l
275.
by mafribe 10y ago
HoTT means a lot to me (lol) HoTT brought dependent types and interactive theorem proving to the masses. Before HoTT, the number of researchers working seriously on dependent type theory was probably < 20. This has now changed, and the f
276.
by mafribe 10y ago
I recommend to look at Cedric Fournet's group [1]. They have (or are close to having) a performant networking stack that's fully verified, e.g. [2]. [1] http://research.microsoft.com/en-us/um/people/
277.
by mafribe 10y ago
There is a big overlap in prover theory. HOL Light comes from Intelite John Harrison. I don't know much about CPUs, but I suspect that one of the core problems of software verification, the absence of a useful specification, isn'
278.
by mafribe 10y ago
True, but China has equivalents of all of them ... if you read Chinese.
279.
by mafribe 10y ago
That depends on your background and your goals. How much do you know about modern testing, abstract interpretation, SAT/SMT solving? In any case, as of Feb 2017, a lot of this technology is not yet economical for non-safety critical ma
280.
by mafribe 10y ago
Compilation: - Meta-tracing, e.g. PyPy. - End-to-end verification of compilers, e.g. CompCert and CakeML. Programming languages: - Mainstreamisation of the ideas of ML-like languages, e.g. Scala, Rust, Haskell, and the effect these idea
281.
by mafribe 10y ago
Timely article (albeit a bit loquacious for my liking). Here's my summary of how my travel has changed from "Then" (pre ubiquitous internet) to "Now". Contact with home: Then: Highly sporadic. Occasional postcard,
282.
by mafribe 10y ago
Lovelace was probably the first to think about using it for something other than pure computation. This is deeply misleading. For example the idea to have automata make music, and more generally for automata to be creative
283.
by mafribe 10y ago
Logical and typing judgements can be presented in many different ways, triples like ∆⊢e:A being one of them.
284.
by mafribe 10y ago
As this paper is about a Curry-Howard correspondence, the statement has two (equivalent) readings. Reading 1. It's a typing judgement. You can read ∆⊢e:A as "the program e has type A, assuming the free variables in e are typed as
285.
by mafribe 10y ago
Singapore has similarly low crime figures and is not remotely as homogeneous as Japan.
286.
by mafribe 10y ago
The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most forms of computation beyond strongly normalising pure functi
287.
by mafribe 10y ago
Thank you, that's an interesting point. The thought that somebody would not be able to understand the type of map had not occurred to me, because I'm surrounded by people with a strong maths/FP background. Shows just how narr
288.
by mafribe 10y ago
can even reason about the composition of logics I'm not aware of a fully fledged approach to logical composition that tells me an interesting story about the combination of logics that arise in computation, I know that peopl
289.
by mafribe 10y ago
Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.
290.
by mafribe 10y ago
Non termination is modeled as false: That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) a
291.
by mafribe 10y ago
programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, co
292.
by mafribe 10y ago
The US had long supported the Allied side sub-rosa, e.g. the sinking of the RMS Lusitania. At least on some interpretations that support amounted to an act of war. Imagine, to put this into perspective, that you had been caught in 2002 to s
293.
by mafribe 10y ago
virtually a declaration of war. Have you reflected properly on why Germany felt a need to defend itself against the US?
294.
by mafribe 10y ago
dearth of learning materials for things like Hindley-Milner What's wrong with the original paper [1]? It's really basic and boiled down to the essence (in true Milner style). I give it to all my students interested i
295.
by mafribe 10y ago
Anyone up for writing such a high-quality book as this one on statically-typed languages, Not a book, but maybe "The Essence of ML Type Inference" by Pottier and Remy [1] is of interest. It's a bit more in-depth
296.
by mafribe 10y ago
While I agree that compilation of dynamically typed languages is more challenging, inference for advanced typing systems is full of problems: - How to ensure that the inference algorithm is correct. - How to design typing systems that are e
297.
by mafribe 10y ago
Rail is typically never profitable unless the increase in land value around stations is captured. This is really interesting. Have you got a pointer for me where I can read more on the economics of railways along those line
298.
by mafribe 10y ago
loose applicability at the first contact When thinking about complex domains, having a simplistic model is helpful for a variety of reasons, one of them is to establish a shared vocabulary to communicate with others, the other is t
299.
by mafribe 10y ago
Wiles' original FLT result was first presented at a workshop in Cambridge, although he didn't explicitly state that he had succeeded (sans the gap) in proving FLT, he left that for the audience to infer.
300.
by mafribe 10y ago
Massive amount of very interesting info Agreed. The most interesting account of the Brexit vote I've read, and one of the most insightful of how modern politics works.

More ›