История изменений

соответственно и практическая рекомендация будет: делать unsafe куски достаточно маленькими и, главное, тривиально доказуемыми, а техническую корректность(а если ещё тайпстейт программинг заюзать то и логическую) программы в целом будет доказывать уже компилятор, и вот это вполне себе правильный и практический эволюционный шаг. А так у нас или spark, agda, coq т.п. плюс фактически полноценный прикладной математик, что очень дорого и долго и оправдано только для жёсткого миссион критикал, или си стайл болото с непознаваемыми блобами которые допинывают тестами до более менее рабочего состояния, и скрещивают пальцы

соответственно и практическая рекомендация будет: делать unsafe куски достаточно маленькими и, главное, тривиально доказуемыми, а техническую корректность(а если ещё тайпстейт программинг заюзать то и логическую) программы в целом будет доказывать уже компилятор, и вот это вполне себе правильный и практический эволюционный шаг. А так у нас или spark, agda, coq плюс фактически полноценный прикладной математик, что очень дорого и долго и оправдано только для жёсткого миссион критикал, или си стайл болото с непознаваемыми блобами которые допинывают тестами до более менее рабочего состояния, и скрещивают пальцы