johnbender

12 ms·

31.
by johnbender 7y ago
Formal specifications aren't only useful for proving properties of programs. They can also be useful for providing definitive answers to questions about example program behavior which is useful for regular programmers. For example the
32.
by johnbender 7y ago
For the memory model you can take a look at some of the best research in the subfield: https://www.cl.cam.ac.uk/~pes20/weakmemory/index3.html
33.
by johnbender 8y ago
See my comment to sibling [1]. In the case of C and the JMM, "proper semantics" is not. [1] https://news.ycombinator.com/item?id=18312101
34.
by johnbender 8y ago
> well-defined atomic primitives The example I gave is simple and relates to the example of the parent but there are more complex cases for which it is a matter of ongoing research to define a semantics that also admits compiler optimiza
35.
by johnbender 8y ago
Compiler optimizations are one of the primary culprits in making it difficult to reason about lock-free programs. Semantics-preserving optimizations in a single-threaded context are not necessarily semantics-preserving in a multi-threaded,
36.
by johnbender 8y ago
> It's the logic of state developing over time. You may already be aware of this, but that various kinds of temporal logic allows one to capture very complex predicates for the evolution of state machine (much like your person with
37.
by johnbender 8y ago
> They use the term to imply that it's men and that they're the dominate population within tech.. which isn't even close to being true This seems to contradict most of the information I've seen in the diversity report
38.
by johnbender 9y ago
Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language [1] I'm going to see the talk tomorrow at POPL, should be good. [1] https://hal.archives-ouvertes.fr/hal-01673536/file/Linear%20...
39.
by johnbender 9y ago
> My third favorite thing is that I can get to work in basically the same amount of time as driving. On my E-Bike, it takes 22 minutes to get to work (7.5 miles). It takes me 15 minutes to drive there. I live about 6 miles from where I w
40.
by johnbender 9y ago
Beyond notation and ordering, I have had the best results reading and comprehending complex concepts, including mathematics, by taking the following suggestion to the extreme: > Read with pencil and paper in hand, making up little exampl
41.
by johnbender 9y ago
Yes! I’m not suggesting they are synonymous, but proofs in coq are definitely formal proofs (as I understand that term/phrase).
42.
by johnbender 9y ago
> At one extreme lies the systems of formal proofs that encode proofs and theorems in an almost unrecognisable language “known only to a bunch of monks that live on a mountain" I haven't read too far but I think this refers to
43.
by johnbender 9y ago
I agree with most of what you say, and I'm sorry I should have been clear that I don't think your comment is without merit. In truth, I am reacting more to the general direction I see in PL discussion on HN (which is what I should
44.
by johnbender 9y ago
It's kind of a bummer to me that the one of the top comments here is about the syntax. I get that people have syntax preferences and that there's a certain level of "sniff" test that goes along with these things, but as
45.
by johnbender 9y ago
These papers take forever to read (take it from me, I am doing research in this area, in particular proofs of correctness for lock free programs). I recommend focusing on the C/C++ ones if only for the practical value. As for compariso
46.
by johnbender 9y ago
It seems like weak memory models get short shrift, but if you're going to program without locks it's semi-important to understand what information one gets when examining a read-write pair. It's true that (as implied by the a
47.
by johnbender 9y ago
I agree. I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer. As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to go
48.
by johnbender 9y ago
Not a stupid question at all! An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't p
49.
by johnbender 9y ago
I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq. UPDATE: found it thank you.
50.
by johnbender 9y ago
A few thoughts/questions if the authors stop by since I can't seem to find a link to the Coq source: I'm curious if there is an interpreter written in Gallina that implements the semantics? Maybe with a simulation proof (or s
51.
by johnbender 9y ago
Not sure if this helps but I hacked this together the other day to avoid adding a real queue to a very simple application. It uses event queue ordering semantics to get FIFO behavior. The read/write combinations to the semaphore variab
52.
Human-Level Intelligence or Animal-Like Abilities?(arxiv.org)
2 points by johnbender 9y ago|0 comments
53.
by johnbender 9y ago
> Thus a multifacetted image of mathematics as a coherent subject, all of whose many aspects are well connected, is important for a successful teaching of mathematics to students with diverse (possible) motivations. Somewhat useless pers
54.
by johnbender 9y ago
Cousin comment helped me out a bunch: https://news.ycombinator.com/item?id=14540054
55.
by johnbender 9y ago
I will try to translate my understanding: > This collection forms an axiom system for the Natural numbers and all true statements are provable in this system. Indeed, every true statement is an axiom. You have defined the axiom system as
56.
by johnbender 9y ago
Worth reading maybe? http://reasoning.cs.ucla.edu/fetch.php?id=136&type=pdf Abstract: > We propose the Probabilistic Sentential Decision Diagram (PSDD): A complete and canonical representation of probability distribu
57.
by johnbender 9y ago
Since we're here maybe I can ask you for clarification/help! When I said "true statements that can't be proven" it should have been qualified to a particular set of axioms. That is, I am claiming each set of axioms
58.
by johnbender 9y ago
I don't think these two things are mutually exclusive. As far as I'm aware there is work underway to take logical constructions and integrate them with probablistic machine learning to do things like force zero probabilities in im
59.
by johnbender 9y ago
Incompleteness means there are true statements that can't be proven. Given that any standard set of "fundamental logical concepts" is probably sound and as long as "all pure mathematics" means "that which can b
60.
by johnbender 9y ago
FSCQ is a really great example of a large system with proofs of correctness using extraction from Coq. Another well known project is CompCert the certified C compiler [1]. Which has seen a fair amount of external testing and use in verifica

More ›