Телеграмм чат группы RSA4096 страница 3476

ну фуксия не модная

22:05пожаловаться #1

Вот там вроде микроядро но не раст конечно

22:05пожаловаться #2

Vyacheslav Goma

ну фуксия не модная

22:05пожаловаться #3

из модного ток си++ в драйверах и микроядро

22:05пожаловаться #4

Gymmasssorla

это немного не про то, у раста нормального тула для верификации нет

А чё те надо

22:05пожаловаться #5

и то мода 1980 годов каких то

22:05пожаловаться #6

ну вон выше кинул микроядро, васм, P2P для всех программ

22:06пожаловаться #7

https://frama-c.com/download/acsl-tutorial.pdf

MrSmith

А чё те надо

22:06пожаловаться #8

Можно запариться и сделать но вроде бы рабочая группа верифицирует как то std

22:06пожаловаться #9

Applied operating system - an operating system kernel written in the ATS programming language. - xlq/aos

https://github.com/xlq/aos вот это модно молодёжно

GitHub

xlq/aos

22:06пожаловаться #10

MrSmith

Можно запариться и сделать но вроде бы рабочая группа верифицирует как то std

я смотрел как там верифицируют. руками переводят в Lean и обратно, такое себе удовольствие

22:07пожаловаться #11

причём перевести ещё правильно нужно кек

22:07пожаловаться #12

Дак ептить вообще это вроде зав типами решается

22:07пожаловаться #13

То что выше

22:07пожаловаться #14

зачем собсна такая верификация лол

22:07пожаловаться #15

required и тд

22:07пожаловаться #16

MrSmith

Дак ептить вообще это вроде зав типами решается

но похуже

22:08пожаловаться #17

бойлерплейта много

22:08пожаловаться #18

а там солвер

22:08пожаловаться #19

внутри