Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

  it required several person-months to implement and verify a generic doubly-linked list library in F*, while it required only three hours to do so in Dafny
This could be deceptive. Structures like linked-lists are fiendishly hard to implement in safe Rust too, but people are able to stay productive by (mostly) not implementing things like that themselves. In Rust's case the difficulty comes from ownership: anything involving complex reference graphs for the sake of traversal is going to be really gnarly to establish a single-ownership story for. I don't know about F*.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: