News for hackers. Stuff that matters.
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by retrac on Monday September 13, 2021 @09:36AM (#28511290)
Not as a monolithic object. You might be able to do it with an almost microkernel approach (whatever you're implementing) with multiple small, well-defined objects with a well-defined protocol between them. That can be very useful. But I doubt you could formally verify their collective behaviour. The space and time complexity of the algorithms is explosive as the number of interacting objects increases.
Re:How We Proved the Eth2 Deposit Contract Is Free of Runtim... by maweki on Monday September 13, 2021 @09:51AM (#28511486)
Note that the specification (what you prove correctness of the implementation against) already grows with the number of interactions.