5 ms·

Very cool idea! What I love about C is that all sorts of programming language can talk to its ABI and that it fits well with low level programming. However it

Very cool idea! What I love about C is that all sorts of programming language can talk to its ABI and that it fits well with low level programming. However it is a cumbersome and unsafe language. This seems like a very nice solution. You can write in a much safer language while producing C code which does not look too alien relative to what you wrote I have been interested in Rust but thinking it looks a tad too complicated. This may be a happy inbetween.

simias 7y ago
I'd expect that a formally provable language would be more complicated to write in practice than Rust. Take this example for instance: >you must tell the compiler that accessing the array at position 2 is defined. quick fix for this one: fn bla(int * a) where len(a) == 3 { a[2]; } In Rust you don't need the where clause, the `a[2]` operation will just panic at runtime if the array is too short. You don't have to prove to the language that the access is correct.
- speps 7y ago
  Except the checks in ZZ are at compile time and have no runtime overhead.
  - Gene_Parmesan 7y ago
    Right, but the question was about which language was more complicated (with the implication being, complicated to write). In that sense I think my GP comment is probably correct.
- dmos62 7y ago
  I've not looked at ZZ yet, but when we talk about formal proofs, we're usually proving much more interesting properties than what a type system typically proves.
- firebacon 7y ago
  > operation will just panic at runtime if the array is too short Exactly, rust doesn't provide a good solution to this problem at all. Panics in rust are an escape hatch used to ensure the language stays "safe" in situations where the compiler can not prove a given behaviour at compile time, but where it would have made the language too ugly if you had to wire through Result types for all the trivial operations like adding two numbers. In my experience, panics in rust have been a major source of pain. In contrast to an exception, which you can catch, a panic behaves more like an abort. At least it has been that way in the past. Now, with a lot of libraries using panics to signalize runtime errors, coding in rust has at some times felt like I was using a bunch of badly written C libraries that internally call "abort()" and kill the process when something goes wrong that would have been totally handle-able without killing the whole process. That's the benefit of using a safe language, right? I think lately the rust "community" has become aware of this issue and IMO the way things are going is that that panics, as they are designed, should basically not be used. But, without proper exceptions, that brings you back to the situation where an operation as trivial as adding two numbers either produces a return code that must be explicitly checked or may silently fail and produce an "undefined" result in some cases.
  - steveklabnik 7y ago
    What libraries are using panics for runtime errors?
  - jcranmer 7y ago
    A panic in Rust nicely captures the category of errors which the programmer asserts should be impossible, which generally cannot be recovered well from. A panic is kind of catchable, but it only works in the sense of killing only part of the process rather than the entire process (like abort does). If errors are expected, then you should Result instead of a panic. If people are using panics instead of Result for these kinds of errors, then the library is wrong. I'm curious what examples you have where this is happening.
wuschel 7y ago
If you like this, it might be worth looking at ATS: http://www.ats-lang.org/ http://www.ats-lang.org/
- throwaway17_17 7y ago
  I'm a fan of ATS, really I am, but recommending ATS to someone who said Rust looks too complicated made me literally laugh out loud. Like I said, I like ATS and don't particularly care for Rust, but ATS is in no way less complicated that Rust. But I really do feel like the laugh I had is going to make my day better, so thanks. Just a note: the above is not sarcasm

simias 7y ago

I'd expect that a formally provable language would be more complicated to write in practice than Rust. Take this example for instance: >you must tell the compiler that accessing the array at position 2 is defined. quick fix for this one: fn bla(int * a) where len(a) == 3 { a[2]; } In Rust you don't need the where clause, the `a[2]` operation will just panic at runtime if the array is too short. You don't have to prove to the language that the access is correct.

speps 7y ago
Except the checks in ZZ are at compile time and have no runtime overhead.
- Gene_Parmesan 7y ago
  Right, but the question was about which language was more complicated (with the implication being, complicated to write). In that sense I think my GP comment is probably correct.
dmos62 7y ago
I've not looked at ZZ yet, but when we talk about formal proofs, we're usually proving much more interesting properties than what a type system typically proves.
firebacon 7y ago
> operation will just panic at runtime if the array is too short Exactly, rust doesn't provide a good solution to this problem at all. Panics in rust are an escape hatch used to ensure the language stays "safe" in situations where the compiler can not prove a given behaviour at compile time, but where it would have made the language too ugly if you had to wire through Result types for all the trivial operations like adding two numbers. In my experience, panics in rust have been a major source of pain. In contrast to an exception, which you can catch, a panic behaves more like an abort. At least it has been that way in the past. Now, with a lot of libraries using panics to signalize runtime errors, coding in rust has at some times felt like I was using a bunch of badly written C libraries that internally call "abort()" and kill the process when something goes wrong that would have been totally handle-able without killing the whole process. That's the benefit of using a safe language, right? I think lately the rust "community" has become aware of this issue and IMO the way things are going is that that panics, as they are designed, should basically not be used. But, without proper exceptions, that brings you back to the situation where an operation as trivial as adding two numbers either produces a return code that must be explicitly checked or may silently fail and produce an "undefined" result in some cases.
- steveklabnik 7y ago
  What libraries are using panics for runtime errors?
- jcranmer 7y ago
  A panic in Rust nicely captures the category of errors which the programmer asserts should be impossible, which generally cannot be recovered well from. A panic is kind of catchable, but it only works in the sense of killing only part of the process rather than the entire process (like abort does). If errors are expected, then you should Result instead of a panic. If people are using panics instead of Result for these kinds of errors, then the library is wrong. I'm curious what examples you have where this is happening.

wuschel 7y ago

If you like this, it might be worth looking at ATS: http://www.ats-lang.org/ http://www.ats-lang.org/

throwaway17_17 7y ago
I'm a fan of ATS, really I am, but recommending ATS to someone who said Rust looks too complicated made me literally laugh out loud. Like I said, I like ATS and don't particularly care for Rust, but ATS is in no way less complicated that Rust. But I really do feel like the laugh I had is going to make my day better, so thanks. Just a note: the above is not sarcasm