Why running Idris apps on seL4?

Idris is a dependently typed pure functional programming languages. In short this means that it is very powerful, which makes it magnitudes easier to write correct code and verify it compared to the normal imperative programs. If a solid application is built on an unstable foundation, it is not so solid anymore, right? To date, there is not a more solid foundation to build applications on than seL4. The reasons can be summed up in these bullets.

  • seL4 contains no implementation bugs in the verified code
  • Dependent types is probably the most powerful way to write correct software
  • It was fun :)

Prerequisites

To build this application the seL4 build system and the Idris compiler needs to be setup.

Get the Code!

Run the following to get the code.

mkdir sel4-idris
cd sel4-idris
repo init -u https://github.com/mokshasoft/sel4-idris-manifest.git
repo sync
      

Build and run it in QEMU

Run the following to build and run it:

make x64_hello-idris-1_defconfig
make simulate
      

After the boot the following should be displayed in the terminal:

seL4 <3 Idris
      

Quit QEMU with 'Ctrl-a c'

Contact

Contact me if you have any questions or comments on seL4, Idris or this tutorial.

+46 707 31 06 27

jonas.cl@protonmail.com