Functional IoT Meetup

Table of contents

• Slide
• Tweets

We had “Functional IoT Meetup #0” that share knowledge about functional programming on embedded device.

Today, many people choose C/C++ language to write code on embedded device. However IoT device is:

• connected to the internet
• developed in a short time
• storing personal data
• secure
• more intelligence
• inexpensive

The language is good to design the IoT devices? I think it’s hard. We need more effective programming language, which is static typing, theorem proving, formal method, design by contract, model checking, static verification, SMT solver for example. We have already had such languages that are not known worldwide.

The Functional IoT Project aims to summarize knowledge of the languages as exhaustive catalog. At the project, we survey existing the methodologies as you like, and write some demo code running on tiny MCU.

The Functional IoT Meetup aims to share the knowledge at the meeting located Tokyo, Japan. After the meetup, we update our exhaustive catalog of the methodologies. At first meetup, we share outline of following methodologies (for more detail, please read slides):

• ATS
• Rust
• Jhc
• Ivory
• Idris
• Ada
• Haxe
• VeriFast
• Coq
• Isabelle/HOL
• Alloy
• ACSL (Frama-C)
• CBMC
• seL4 microkernel
• eChronos RTOS
• Redox
• Mirage OS
• AOS

Then, we have some feedback from the first meetup:

• Try to understand seL4 and VeriFast.
• Would like to try Rust for embedded programming!
• Share knowledge to design device drivers.
• Share knowledge for embedded programming.
• How to prove embedded code with some behavior?
• When we can stop the proving in detail? What is reasonable to prove?
• Developing from scratch is nonsense. What is good interaction between the language and C language?
• What is good amount of proving? Proving anything is impossible in actuality?

We will plan next meetup soon.

Slide

Tweets

関数型IoTプログラミング勉強会 第0回 まとめ - Togetterまとめ