unboxed_type

8 ms·

31.
by unboxed_type 9y ago
Thou shall embrace the true power of functional programming
32.
by unboxed_type 9y ago
What is your motivation behind that activity?
33.
by unboxed_type 9y ago
It looks like we have a misconception of the verb "to learn". Conveying some very general intuition of the subject from adult to a kid is not learning, actually. Learning assumes conscious effort to comprehend relatively complex t
34.
by unboxed_type 9y ago
Nice idea for a toy! But learning an internal machinery of that process isn't that fun if you are not inclined for that kind of activity.
35.
by unboxed_type 9y ago
>I personally prefer hand-written recursive descent parsers >using a parser combinator framework (like https://github.com >/Geal/nom) over parser generators. Why?
36.
by unboxed_type 9y ago
Please let Five-Year-Olds play their toys instead of learning calculus, so they can grow up healthy people.
37.
by unboxed_type 9y ago
Your observation about correspondence between algorithmic complexity and its structure seems very interesting to me, thanks for sharing.
38.
by unboxed_type 9y ago
Scala is different in that it has stronger type system, automatic memory management, the language is well-specified and is based on JVM, a reliable runtime. I would suggest that even Java would be much better choice than C++ for that projec
39.
by unboxed_type 9y ago
I agree with most things you said, however. > Lean is written in pretty principled C++. For how long this will last? Many will agree here, that C++ is known for its ineptitude for "long-term" projects where maintenance issues
40.
by unboxed_type 9y ago
I would love Lean to become both reliable and fast tool. I suggest, it is in its infancy right now to judge it seriously. As for now, I would rather invest in well established tools.
41.
by unboxed_type 9y ago
>Note that none of those code extractors are verified to be >correct themselves, lacking a formalization of the target >language's semantics. CertiCoq project aims to provide a certified compiler from Coq into CLight (formaliz
42.
by unboxed_type 9y ago
"The compiler itself is also written in Scala and its underlying Coq parser is largely based on the use of parser combinators" while "true" extractor has to be written in Coq, as I understand :-)
43.
by unboxed_type 9y ago
Correct.
44.
by unboxed_type 9y ago
I wonder why they have not used Coq's extraction approach?
45.
by unboxed_type 9y ago
Absolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.
46.
by unboxed_type 9y ago
Have you tried it yourself or maybe you know someone who have? Honestly, I think that this development is highly impractical due to very high entrance ticket price for someone not belonging to UW PLSE group ;-)
47.
by unboxed_type 9y ago
Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the au
48.
by unboxed_type 9y ago
Thanks for the reference.
49.
by unboxed_type 9y ago
Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed syste
50.
by unboxed_type 9y ago
What about real CPUs (much more complex than 'Forth CPU'), network adapters (has its own CPU), memory controllers, real OS kernels, POSIX library (which is sometimes loosely specified) and so on? As far as I understand modern trul
51.
by unboxed_type 9y ago
How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to preven
52.
by unboxed_type 9y ago
Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks v
53.
by unboxed_type 10y ago
Yes, but what if you are unable to explore the whole state space due to its unboundedness? Then the only way I know is by deducing properties thru temporal reasoning.
54.
by unboxed_type 10y ago
Sounds interesting! I would definitely join that forum. This sounds like a new kind of sci resource with well-defined purpose.
55.
by unboxed_type 10y ago
Researcher has to have some amount of authority in his field to receive grants. Publishing in high-tier venue is a good way to get that authority because it is how people-with-money judge researchers :-) Well I really enjoy reading articles
56.
by unboxed_type 10y ago
Temporal reasoning is a lot more than that you mentioned, so by providing this example you can not conclude that TLAPS support temporal reasoning. I have read several papers of S.Merz, Lamport's student and now a researcher, who mentio
57.
by unboxed_type 10y ago
AFAIK, TLAPS does not support temporal reasoning in full currently, so you are not able to prove liveness properties of your system. On the other hand, Coq is able to express both LTL logic and infinite trace, so you can prove such things i
58.
by unboxed_type 10y ago
I hold a "senior researcher" position at research dep. of one of security-related IT companies. I am developing a TLA model to specify one of companies product core protocols. My previous job title was "senior distributed sys
59.
by unboxed_type 10y ago
Well personally I would rather suggest to write a model, not a rigorous proof. A formal proof of any real protocol is both long and tedious journey; production guys will hardly find it useful thing to do. On the other hand a logical model c
60.
by unboxed_type 10y ago
I am no academic, but I read a lot of papers and going to write one this year. I skimmed the paper without getting into details about the protocol itself, but made some observations about the paper in general. My personal very subjective op

More ›