Porting a formally proven Tetris to a Pebble smartwatch in Ada | Hacker News Reader

Porting a formally proven Tetris to a Pebble smartwatch in Ada

blog.adacore.com

67 pointsiamwil27 comments

This blog post seems to be coming from an alternate universe where OS APIs are "very well thought out" and we program in sane languages and correctness is valued and formal methods are used and software is actually good.

In other words, France ;-)

The land of OCaml!

And Eiffel and Bertrand Meyer!

And Prolog.

The jury is still open about Prolog vs Planner isn't it ?

How do you mean that? I'm not sure.

That planner was superior and prior Prolog.

Prior, yes. Superior, how?

I give the French credit on that angle. They're certainly in the lead for practical R&D + tools for building and verifying software. Especially anything coming out of INRIA or Meyer's teams.

I never heard of AdaCore being French, though. Only two of the Executive Team (below) were educated in France with most of them (and Ada itself) coming out of U.S. (esp NY). Headquarters is split between the two at least in Contact page. I could be way off so anyone feel free on input to this.

http://www.adacore.com/company/about/executive-team/

French Univ tried their best to teach the good stuff. We had Ada, Scheme, OCaml. Too bad it looked like esoteric dust for many compared to the Java Juggernaut. From the few I've seen it seemed large system became a synonym for UML, not generic formal modular approach. But I left this around 2008, maybe the winds have changed.

I wonder how much 'fresh' Ada is done today (classes, new projects, etc)

All good choices. I'm glad they tried at least. I'm not sure about France but in U.S. universities are expected to give people the job skills they need. Pascal might be easy to learn with and Scheme might be more ideal. Yet, most jobs were using Java or C++ so many schools switched to using those. People start from day 1 thinking that's how programming and design are supposed to work. Kind of sad.

I'm not arguing universities should be impractical. I just encourage them to teach both what's beneficial to the mind and quality of our industry plus the practical tech. Increases odds good things will spill-over from one to the other.

That's the underlying tension. It's hard to avoid, I think it has detrimental effect on the whole industry. Unless schools were sure of the skills transfer from Ada/Scheme to Java/.Net or whatever tech used on a job they could enforce better education of better concepts rather than ensuring a easier to sell resume. The market decided the other way around.

Well, MIT started the Scheme for education thing with SICP/6.001 (https://en.wikipedia.org/wiki/Structure_and_Interpretation_o...) in the early '80s, the thesis being that you could start fresh with it, no introduction to computers or the particular language used in the course, and get right to business, instead of wasting half the class between learning a more complex and picky syntax and fighting with the language to express things not natural to it.

It's also default interpreted, so the write code->run code cycle is instantaneous (although the ones MIT used had compilers, and nowadays machines are so fast LISPs tend to immediately compile everything typed into the REPL). Typing is of course important, the argument here is that for initial education, dynamic typing when these small programs are run is better than adding the complexity of declaring types, especially since so few are needed in an introduction course.

A CS (and EE, i.e. 6-3) or EECS (6-2, what most students major in today) major would learn CLU, later Java, when they took either the software engineering or compiler course. And of course there were many opportunities to learn languages and get paid for programming, including the co-op program, which is now mostly formalized into a MEng program that most students do.

The dot.com crash cratered EECS enrollment, which had been steady at 40% of the undergraduate for decades, it dropped by more than half. People panicked, Lisp haters made sure all of it was expunged from required undergraduate courses, and MIT just plain changed what it meant to be a MIT EECS graduate. With a lot of surface politeness, here's one for the record explanation: http://www.wisdomandwonder.com/link/2110/why-mit-switched-fr...

It's now much more about making gadgets than, oh, trustworthy libraries. Pity almost no one, proprietary or FOSS, provides any of the latter. A portion of 6.001 is taught by the 6.001-zombies in January, with credit available for the first N who sign up, as 6.037, and if you don't know Python when you arrive, there's courses which will teach you it before you take the new 6.01 that pretends to start replacing 6.001.

Or, if you're really serious about pure CS, you're likely better off going to some place like CMU if you can get into the program. (I got the impression some years ago when CS became popular again that Stanford is more like CMU and U.C. Berkeley more like MIT, but I don't know if that's true or still true. If you're serious about CS and can't get into one of those 4 best in the world with no one close behind, you should think very carefully about your path forward.)

Wow, that was some quote by Sussman. Terrible. However, they will be more skilled at dealing with the crap industry will throw at them.

Far as trustworthy, at least we're seeing a minor resurgence of that. I write about many of those techs. I think Ocaml community is one of best examples. There's an inherently robust language, a good compiler, integration with formal methods via Coq extraction, smart academics invested in it, uptake in industry (i.e. Jane St), and mainstream uptake to a degree. Leroy et al have something really good going on there.

Need more academic stuff like that.

My old univ caved in too. They retired the lisp/recursive introductory course for a python one centered on component/libraries IIUC.

At least Python is one of the higher quality languages and codebases to go mainstream. The code they make might at least be readable...

The biggest problem I see with it is the author's allergy of functional programming. He even attempted to remove some of the existing ad hoc FP features in the move to Python 3 or the like. Hence my comment about wasting time fighting the language.

It plus Java, as MIT and I'm sure many other schools do (those that aren't just pure "JavaSchools") are going to leave students who don't make extra effort ... deficient when it comes to FP, the virtues of which I don't need to extol to you, although I'll add that it seems to be one of the good answers to making the most of our current "Moore's Law maybe", "Dennard scaling no" multi-core situation.

I came from an imperative background so it didn't bother me so much. I agree it makes people suck at FP. Least there's good free work like "How to Design Programs" with the Racket tools. Should give them a nice boost.

However, there's lots of ways to scale. FP is better at it but not necessary. It's easier for a decent imperative programmer to learn to scalable concurrency than to learn FP. So, path of least resistance & backward compatible means that non-FP approaches should get most traction. That's what we see in practice.

Good news is that your point got many interested in making an attempt and led to more FP developers + languages. I even saw a case study of a company in finance using Haskell for production due to concise, correct, and concurrent properties. Plenty potential here.

Jeez, I remember in college in the 80's we were wondering if there would ever be decently-performing Ada on an MS-DOS machine. Now it's compiling to a watch :)

Things come a long way, eh? And another team got Ocaml on an 8-bit PIC:

http://lambda-the-ultimate.org/node/5232

High-integrity languages are certainly getting more efficient. Just makes it more fun for me when I'm told how they're "too inefficient" for systems work by C fans. ;)

The title of the article is awful, the article is about porting Tetris to a Pebble smartwatch, the fact the code is formally proven isn't important.

On the contrary, the article is all about promoting formal methods and in particular Adacore's tools. I agree that including Tetris in the title (like the previous article did) could attract more people.

If that was the intention, a better title would be 'Running formally-verified code on the Pebble smartwatch'.

We've put that info in the title. If someone suggests a better title we can change it again. (Submitted title was "Formal proof on a Pebble smartwatch in Ada".)

Thank you dang.

Nice writeup on the game and application of lightweight, formal methods.

Reply on news.ycombinator.com