6 ms·

Porting a formally proven Tetris to a Pebble smartwatch in Ada

67 points by iamwil 11y ago

wk_end 11y ago
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.
- junke 11y ago
  In other words, France ;-)
  - gaius 11y ago
    The land of OCaml!
    - criddell 11y ago
      And Eiffel and Bertrand Meyer!
      - YeGoblynQueenne 11y ago
        And Prolog.
        agumonkey 11y ago
        The jury is still open about Prolog vs Planner isn't it ?
        YeGoblynQueenne 11y ago
        How do you mean that? I'm not sure.
        agumonkey 11y ago
        That planner was superior and prior Prolog.
        YeGoblynQueenne 11y ago
        Prior, yes. Superior, how?
  - nickpsecurity 11y ago
    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/ http://www.adacore.com/company/about/executive-team/
    - agumonkey 11y ago
      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)
      - nickpsecurity 11y ago
        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.
        agumonkey 11y ago
        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.
deleted 11y ago
[deleted]
ZenoArrow 11y ago
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.
- junke 11y ago
  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.
  - ZenoArrow 11y ago
    If that was the intention, a better title would be 'Running formally-verified code on the Pebble smartwatch'.
- dang 11y ago
  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".)
  - ZenoArrow 11y ago
    Thank you dang.
johnhattan 11y ago
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 :)
- nickpsecurity 11y ago
  Things come a long way, eh? And another team got Ocaml on an 8-bit PIC: http://lambda-the-ultimate.org/node/5232 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. ;)
nickpsecurity 11y ago
Nice writeup on the game and application of lightweight, formal methods.

67 points by iamwil 11y ago

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.

junke 11y ago
In other words, France ;-)
- gaius 11y ago
  The land of OCaml!
  - criddell 11y ago
    And Eiffel and Bertrand Meyer!
    - YeGoblynQueenne 11y ago
      And Prolog.
      - agumonkey 11y ago
        The jury is still open about Prolog vs Planner isn't it ?
        YeGoblynQueenne 11y ago
        How do you mean that? I'm not sure.
        agumonkey 11y ago
        That planner was superior and prior Prolog.
        YeGoblynQueenne 11y ago
        Prior, yes. Superior, how?
- nickpsecurity 11y ago
  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/ http://www.adacore.com/company/about/executive-team/
  - agumonkey 11y ago
    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)
    - nickpsecurity 11y ago
      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.
      - agumonkey 11y ago
        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.

deleted 11y ago

[deleted]

ZenoArrow 11y ago

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.

junke 11y ago
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.
- ZenoArrow 11y ago
  If that was the intention, a better title would be 'Running formally-verified code on the Pebble smartwatch'.
dang 11y ago
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".)
- ZenoArrow 11y ago
  Thank you dang.

johnhattan 11y ago

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

nickpsecurity 11y ago
Things come a long way, eh? And another team got Ocaml on an 8-bit PIC: http://lambda-the-ultimate.org/node/5232 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. ;)

nickpsecurity 11y ago

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