Design OS with full FL or Fl sematics

Can we use Fl to build a OS , or build a OS with FL semantic with any language you like?

In this way, reasoning of OS will be much easier.

In fact, the value of FL is to force people to think in Fl way, which is easier to be reasoned.