xgk

17 ms·

31.
by xgk 9y ago
I wish you had elaborated this comment into something substantial that readers could learn from. Here is an interesting comment that a classical composer -- possibly the most influential one in the 20th century through his students -- on Ap
32.
by xgk 9y ago
That is a controversial point and depends on your concept of art. There are conceptions of art where novelty is an integral part of the very definition of artwork. I agree that pop-music is precisely about creating "feeling and atmosph
33.
by xgk 9y ago
Why would a "link" be interesting or relevant? My point that modern pop-music is extremely generic stands/falls whether I have "tracks" or not. It's hard to deny that modern pop-music is to an extremely good ap
34.
by xgk 9y ago
Beethoven would be making techno Why? Given that making techno, or modern pop music in general, is basically trivial. Just spin up Ableton, press a few buttons ... boom, 10 minutes later you've got a competitive techno-track t
35.
by xgk 9y ago
It's hard not to be reminded of Mao's Hundred Flowers Campaign (百花运动) [1] and Anti-Rightist Movement (反右运动) [2]. [1] https://en.wikipedia.org/wiki/Hundred_Flowers_Campaign [2] https://en.wikipe
36.
by xgk 9y ago
One of my PhD students will soon have to learn an interactive prover. I was to recommend Isabelle/HOL because it's got the best automation, but maybe I should consider Lean (and learn it along with him). I worry slightly about Lea
37.
by xgk 9y ago
calling context In compositional verification, you generally want to prove as much as possible about the piece of code at hand -- irrespective of calling context. spec very similar to this Yes, I was using something similar
38.
by xgk 9y ago
Thanks for the link to the paper. De Moura is giving a talk tomorrow in Cambridge at the workshop in computer aided proofs called "Metaprogramming with Dependent Type Theory". I wanted to go, but won't be able to attend. I gu
39.
by xgk 9y ago
Depending on the programming language being proved That's true, GCed languages are simpler in this regard. But for low-level languages you have to do this 'by hand', and it can be complicated. not had the co
40.
by xgk 9y ago
Yes. Mostly. But in practise, you need to specify what sortedness means, and in a generic sorting algorithm that means axiomatising the comparison predicate, including its side-effects. Note for example the C standard library implementation
41.
by xgk 9y ago
there is only a "theorem" datatype You mean that there is NOT only a "theorem" datatype? In contrast to Curry/Howard provers, the LCF approach forgets proofs, it guarantees soundness by giving you acces
42.
by xgk 9y ago
The latter ones can be all incorrect for all you care Good point. Maybe we can call this the TSP (trusted specification base)? In my experience the TSP is subtle and contains most of the intermediate definitions too. A few
43.
by xgk 9y ago
This is interesting. It will take me some time to digest this paper. As an aside: is there a terse description of Lean's type-theory? Also: Lean is Curry/Howard based, it's not an LCF-style architecture?
44.
by xgk 9y ago
ITTs like Lean are more expressive as logics than HOL, but I doubt that Certigrad needs even a fraction of HOL's power. So anything you need that you express as types in Lean you should be able to express as theorem in HOL. Presumably
45.
by xgk 9y ago
A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belief. Instead I conjecture that on average the full specification of an a
46.
by xgk 9y ago
Can this be done with Coq? This can be done with any prover. Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1 :: A -> B and f2 :: A -> B, say one slow and simple (f1), one f
47.
by xgk 9y ago
I second this. Isabelle/HOL has much better proof automation than any prover based on Curry/Howard. That's primarily because HOL is a classical logic, while Curry/Howard is constructive (yes, I know we can do classical p
48.
by xgk 9y ago
specification is a lot smaller than the code I doubt that this is the case in general. How can the (full) specification of a program be smaller than the program? This would mean we can always compress a program into a smaller p
49.
by xgk 9y ago
Could this problem have been (partly) avoided by going for an LCF-based prover such as HOL or Isabelle/HOL, rather than a system based on the Curry-Howard correspondence?
50.
by xgk 9y ago
Our model can be used as a basis to implement any approach to hygiene that is of interest.
51.
by xgk 9y ago
We have an implementation in Nominal Isabelle/HOL, but it's not used in the paper.
52.
by xgk 9y ago
Hygiene is deliberately omitted . Why? Because there are various different ways of handling hygiene, including not providing hygiene at all. A foundational model of MP should not 'hard-code' any specific approach towards hygiene.
53.
by xgk 9y ago
Coauthor of the "Modelling ..." paper here. Happy to answer questions!
54.
by xgk 10y ago
The maglev station at Shanghai airport tells you clearly when the fast ones are going. The experience of going so fast so close to the ground is quite maginficent. I was wondering why the cars 'stop' on the nearby motorway.