This year is learning deeply ATS proof for me. Unfortunately, I can’t create any products for Metasepi project, however the learning was very fun. Let’s look back on 2015, and dream next year!
I start to write textbook of ATS language named “ATS Programming Foundations”. Writing the document stopped at September, 2015. Please keep going me…
list of the things done
Nothing.
I introduced ATS language in Japanese local academic meeting “PPL 2015”.
list of the things done
I translated examples of Book “Getting Started with Arduino” into ATS lanugage. The project is arduino-ats and seed for paper “Arduino programing of ML-style in ATS”.
list of the things done
I tried to use Rust language on mbed platform. It needed many “unsafe” keyword and didn’t have well-established method to build binary without run-time. Then, I stopped to use Rust in embedded system, more.
And I tried to translate “Software Foundations Prop_J: Propositions and Evidence” into ATS. It was good idea to compare ATS with the other languages such like Coq. Also I believe that comparing view of ATS with Rust or doing statics of it with Alloy will be useful to understand ATS.
list of the things done
I created palindrome library in ATS to understand proofs of ATS. It became seed for presentation “ATS/LF for Coq users”.
list of the things done
This month, I had an idea to create merge sort using proof and linear type. The idea’s base is that “in-place merge sort” can be shaped using some proof and linear type. Why need such library? The purpose was to get proof of concept for proof driven development on Arduino Uno platform can’t use any malloc. But the implementation is very complex, and can’t be managed by me… Next time, I should take an approach what primary create code with linear type without proof, and secondary re-fine the code with proof.
And these days, I suspected that applying proof to big software architecture is impossible. I think ATS language needs better proof engine at least. Is it the patsolve using Z3? Or ATS needs tactic like Coq?
An example proof for big software architecture is seL4 OS what should be surveyed next year.
list of the things done
Fortunately, I had chance to visit Hongwei’s research room. The local meeting is exciting for me!
list of the things done
This month, I published most valued presentation “ATS/LF for Coq users”, that introduces proof in ATS language with examples. I needed half year to understand it deeply.
list of the things done
Nothing.
This month, I published valued presentation “Static typing and proof in ATS language”, that explain statics in ATS with example of rock-paper-scissors library. Using the presentation, I can understand dynamics/statics/proofs clearly.
ATS programming on ESP8266 was started. I would like to create a good demo movie to tweet over Wi-Fi and IFTTT.
list of the things done
I tried to survey Smart.js. I believe that using JavaScript on MCU doesn’t make sense, however Cesanta’s middleware has good quality. The middleware will be useful on Functionl IoT projects.
I found VeriFast verifier what puts precondition and postcondition in comment of C language. I believe it can also do Programming with Theorem-Proving, such like ATS. VeriFast programming on Arduino was started. Today, the demo code only verifies parameters, but I’ll try to apply more proof. Big negative aspect of VeriFast is that it’s not open source project.
list of the things done
Today, I’m having following to-do list:
Primary challenge will be hosting Functional IoT meetup monthly. Today, we don’t have documents what widely covers formal methods of embedded system. We are not researcher, and engineer. We would like to get soundness and safety for production, and have no time to shape these. I think trade show is needed to get the documents. How about collect up a chart what has vertical axis of software stack and horizontal axis of hardware platform, while create many projects such like ATS programing on Arduino? For example, ATS and Ivory can be used on 8-bit/16-bit/32-bit hardware platform, however jhc is only for 32-bit hardware. The other to-do should be managed under the meetup.
Secondary, I would like to get environment on that all people easily program LED blinking using functional language on tiny MCU such like Cortex-M series and 8-bit Arduino. We should support Arduino, mbed and ESP8266 as the hardware platform.
To find not-understanding methods such like seL4/VeriFast in the early stages is good idea. “Related Languages” on Whiley is useful for it.
May the new year bring us happiness!
blog comments powered by