NuttX #5
Description
Поки з читиком організаційні питання тривають,
пропоную тут обсудити https://x.com/5htco/status/1950485372363739590
Цікаві всі деталі, як технічні так організаційні.
По технічним одразу: верифікація на MLTT це надійніше але x20 по часу від того що можна зробити на SystemF.
пайпайн буде як в L4
Тут не зрозумів, що мається на увазі.
Особисто я з Haskell почати можу просто зараз, з OCaml треба пару днів згадати його. Для доведення метавластивостей Haskell дещо зручніше завдяки higher kind типам, трохи меньше треба енкодити, трохи меньше бойлерплейту. Coq це тиждень-два поразбиратись з його лібами. Anders -- дуже крута ідея, думаю як розкочегаримось, можна в решті як-раз його й використати.
На чому реалізацію нашого NuttX написано, C, й під яку платформу (можливо, це буде важливим на низькому рівні)?
Щодо доведення на апаратному рівні -- це може бути важливо але досить складно, сходу не бачу як це робити (виразити апаратну спеку як рантайм чи стейт-машину?).
Потрібно доведення існування тайм тревел дебагера бо RTOS повинна забезпечувати детерміністичну поведінку при переключенні контекстів IRQ/SCHED.
На ці IRQ/SCHED є спека? Чи документація? Якщо ні, де можна поразбирати їх код?