unboxed_type

What is your motivation behind that activity?

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 things, constantly overcoming pain of uncertainty, most mathematicians will agree with me here. This is not what is usually expected from a kid. Don't do that.

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.

>I personally prefer hand-written recursive descent parsers

>using a parser combinator framework (like https://github.com

>/Geal/nom) over parser generators.

Why?

Please let Five-Year-Olds play their toys instead of learning calculus, so they can grow up healthy people.

Your observation about correspondence between algorithmic complexity and its structure seems very interesting to me, thanks for sharing.

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 project.

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 are of crucial importance. I presume that proof assistants belong to that class. If Leo is the only developer of this project for the rest of life, then it is OK, I guess.

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.

>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 (formalized subset of "Safe C"). In this respect,

it is superior to what you have mentioned, I guess.

Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous,

I feel doubt in its reliability.

"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 :-)

Correct.

I wonder why they have not used Coq's extraction approach?

Absolutely. Anyway this gap is worth mentioning for deeper understanding of a verification problem.

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 ;-)

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 author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.

Thanks for the reference.

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 system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

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 truly reliable system (commerical avionics-like) still must be relatively simple to be verified up to hardware level.

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 prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?

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 very similar?

I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verification.

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.

Sounds interesting! I would definitely join that forum. This sounds like a new kind of sci resource with well-defined purpose.

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 from top-tier venues (PL theory). It means that committee does a good work filtering and improving articles, definitely not without mistakes.

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 mentioned that there is no temporal reasoning apparatus available in TLAPS. Maybe something have changed since then but I found no evidence for this.

> They just use the model checker, that can check

> liveness, too

This is not quite true. Liveness is about infinite number of states, but any real model checking is bounded by definition.

For an engineer this is not a problem at all, but as for comp.sci researcher your ability to use TLA+ is limited in this respect.

> Lamport has repeatedly said "temporal logic is evil"

Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.

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 in it.

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 systems developer"; I was doing a similar thing there.

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 can be encoded in a rather short amount of time by someone who is doing it periodically.

This hypothetical guy could benefit from this activity by co-authoring the paper. Original authors would benefit from it by reinforcing both the protocol and the paper.

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 opinion on how the paper might be reinforced is presented below.

1. Add a system model description under which your protocol is expected to operate.

2. Add description of fault-tolerant properties of the protocol.

3. Do you plan to prove correctness of the algorithm more formally? Maybe you could model the algorithm before publishing. If you prove a safety property using model checking it could considerably reduce doubt about an algorithm correctness.

Good point. As far as I know there are no DO-178B complient C++ libraries available yet (STL, for example). If you know any please point out. My reasoning is as follows: While civil avionics must comply with regulatory safety standards, military avionics is not. So economically speaking there is a little sense for them to do such costly certification just to ensure quality.