>>>>> "Isaac" == Isaac Beckett <isaactbeck...@gmail.com> writes:
Isaac> Are those Haskell sources used to generate the C code, or are Isaac> they an older version of the spec, or something? This is my Isaac> first time hearing of them, so not sure what they’re used for. They were written as the first kernel version, as an executable spec. If you read the paper, https://trustworthy.systems/publications/nictaabstracts/Klein_AEMSKH_14.abstract it tells how seL4 was developed, and where the Haskell prototype fits in. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
