← Back to context

Comment by Solar19

7 years ago

Yes, I like them a lot. A formally verified OS should be the standard these days (and formally verified compilers). But for that to be so, we'll need new programming languages (not Rust) and toolchains I guess.

7 comments

Solar19

Reply
steveklabnik  7 years ago

Why not Rust?

  • Solar19  7 years ago

    So I'm coming at this from a social science perspective. Why did I say "not Rust"? I'm working on a research program to get at what happens when people engage with programming for the first time, aspects of language design that attract or repel learners, and as sort of a related offshoot, why smart women are so disproportionately less interested in programming.

    One of my working hypotheses is that programming is terrible. More precisely, the majority of (smart) people who are introduced to programming have a terrible experience and do not pursue it. I think many smart people walk away thinking that it's stupid – that the design and workings of prevailing programming languages are absurd, tedious, and nonsensical. (Note that most men aren't interested in a programming career either. So it's not just smart women.)

    Most intro to CS or programming courses seem to use Java these days. That's an unfortunate choice. To veteran programmers, Rust likely seems very different from other languages. Its default memory safety, ownership and borrowship and other features are innovative. (Though the amazing performance of Go's garbage collector seems to weaken the case for Rust's approach somewhat.) However, to new learners, I'm pretty sure Rust will be awful. It's fully traditional in its mass of punctuation noise, just saturated with bizarre (to outsiders) curly braces and semicolons. It also has, in my opinion, extremely unintuitive syntax. I see it as somewhat worse than Java in that respect.

    Honestly, Rust is brilliant in more ways than one. I just think they punted on syntax and punctuation noise. I think our timeline is just weird and tragic when it comes to programming languages. They're almost all terrible and just so poorly designed. There's hardly any real scientific research on PL design from a human factors perspective, and what research there is is not applied by PL designers. PLs are just the result of some dude's preferences, and no one seems to be thinking outside of the box when it comes to PL design. In the end, to really make progress in computing and programming, we might need outsiders and non-programmers to design PLs. I'll say that the now-canceled Eve programming language project is a notable exception to the consistent horribleness of modern PLs. We need a few dozen Chris Grangers.

    • grumdan  7 years ago

      Is it really important how easy it is to learn a language when we are talking about formally verified operating system kernels? Beginners are probably not going to write formally verified code, let alone formally verified system code, so this area is already only accessible to veteran programmers who may not have a problem with these aspects of Rust.

      I don't think it's a contradiction to introduce people to programming with more "elegant" or uniform languages that are closer to math (like Scheme or Haskell), or "easy" languages like Python, and then have them move on to Rust if they want to do system-level programming.

      1 reply →

    • steveklabnik  7 years ago

      Thanks, that's very interesting!

      We did think a lot about the syntax, but we wanted to choose something that'd be familiar to existing systems programmers. It's largely based on C++ and Java, with a little bit of ML thrown in. This is because the language is, in many senses, C++ with some ML thrown in.

      > We need a few dozen Chris Grangers.

      Agreed :)

  • zozbot123  7 years ago

    AIUI, proper program verification is still a very long-term goal for Rust (and most of the related short-term effort is currently going into building a formal model for the language, including its "unsafe" fragment). So, "not Rust" in that Rust simply doesn't cut it at present, whereas other solutions (Idris, Coq, even Liquid Haskell) might be closer to what's needed.