Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Jonathan Blow on Rust

np.reddit.com

Post reply on HN
Print view View original

31–40 of 52 posts

Re: Jonathan Blow on Rust

#31

Post by _vdpp »

csb6 wrote: post #20
kentonv wrote: post #18

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS…

I really like this idea. I’ve been messing around with the z3 theorem prover, and while I don’t think there’s an easy way to integrate it to do compile-time checks, I made a little wrapper class that lets you add assertions which are checked for satisfiability at the end of a function’s scope. But it’s all at runtime, so it’s more like a more advanced assert() than anything like Jai or Rust has. I think SMT solvers a…

You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, including Z3 and CVC4. If you run into something that SMT can't figure out in a reasonable time-frame, you can use Coq to manually-prove your theorems too.

Languages like SPARK and Frama C generate Why3ML as an intermediate output that then gets transformed to run against whatever solvers are available during the verification phase of development. Since the verification/proof phase is separate from compilation, you can write your code with fewer checks initially, and then add conditions as you go to prove functional correctness.

I'd be surprised if C++ is ever touted seriously as a language suited for formal verification. I think the language just has too many corners and escape hatches to be able to nail down its semantics in a way that automated provers can handle.

Having said that though, I'm pretty sure the MSVC Driver Verifier tool uses an SMT solver to try and prove the absence of certain types of errors, so who knows?

Re: Jonathan Blow on Rust

#33

Post by kristianp »

Here's a link to the actual podcast he appears in. Not my most productive almost-3 hours while I listened to that. Lots of references in the show notes on that page too:

https://oxide.computer/blog/on-the-metal-9-jonathan-blow/

He also has some things to say about the (wrong in his opinion) direction we've taken in moving to managed and dynamic languages, in that they're not necessarily higher level languages, just more removed from the CPU.

Re: Jonathan Blow on Rust

#34

Post by 7thaccount »

kentonv wrote: post #18

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS…

I think Ada + Spark has something along these lines.

https://www.adacore.com/about-spark

Re: Jonathan Blow on Rust

#35

Post by Dontrememberit »

kentonv wrote: post #18

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS…

> I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works.

Did you take a look at ATS?

Re: Jonathan Blow on Rust

#36

Post by Dontrememberit »

kentonv wrote: post #27
Polyisoprene wrote: post #24

Earlier quoted context omitted.

Would dependent types help in this case? Add the reference type when creating the type and then you could have the compiler check that the contract holds.

It might be expressible with dependent types. I think what I'm suggesting ought to be able to express a superset of dependent types. I think a lot of type theory tries too hard to have certain "desirable" properties, like being decidable (that is, type checking will always complete in finite time). IMO it's fine if there are cases that will go into an infinite loop, as long as the developer has tools for debugging an…

Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether)

That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".

Re: Jonathan Blow on Rust

#37

Post by kentonv »

Dontrememberit wrote: post #36
kentonv wrote: post #27

Earlier quoted context omitted.

It might be expressible with dependent types. I think what I'm suggesting ought to be able to express a superset of dependent types. I think a lot of type theory tries too hard to have certain "desirable" properties, like being decidable (that is, type checking will always complete in finite time). IMO it's fine if there are cases that will go into an infinite loop, as long as the developer has tools for debugging an…

Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether) That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can…

Sorry, I don't understand.

Does this non-terminating function run at compile time or at runtime?

If it runs at compile time, and it doesn't terminate, then presumably no executable is generated? That's good enough for me.

Or are you describing a function that checks some property at runtime, which the type system then depends on afterwards? But if that function never returns, then the subsequent code that depends on the property it was checking won't ever execute. So a false thing is only proven true in code that never executes. That seems fine to me.

(Also note that as a practical matter I mostly don't care if it's possible for a developer to maliciously trick the type system. I only care about catching accidental errors. Relying on a complex type checker for sandboxing of malicious code seems too risky.)

Re: Jonathan Blow on Rust

#38

Post by YatoRust »

lubesGordi wrote: post #5
mlthoughts2018 wrote: post #2

It just seems really unconvincing to me. Just don’t do data modeling with entity pointers at all, and use patterns like RAII to guarantee that resources manage the lifetime of pointers they need. Or use pure functional programming if it matters that much in a given use case. When the article says the compiler doesn’t know whether a given pointer is meant to be an entity pointer or not, but that you do as the programm…

I think most of the time you're right, but in particular in game programming you know the optimizations you're going to need since the patterns have been pretty well established by now. And those patterns and optimizations are pretty low level which requires you to really understand how things are laid out in memory and rust might not give you great insight into how it lays things out (or it's not as well known or ta…

You can lay out your types exactly how you want in Rust, just by using the `#[repr(C)]` or `#[repr(packed)]` attributes to guarantee an ordering of the fields. So,

> rust might not give you great insight into how it lays things out

Is not true, and this is one of the first things you will learn when you try any sort of FFI. So

> (or it's not as well known or talked about...)

Is not true.

Re: Jonathan Blow on Rust

#39

Post by kentonv »

Dontrememberit wrote: post #35
kentonv wrote: post #18

I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. In the Cloudflare Workers runtime we have a sort of analogous problem to what Blow has in his game engine. We have certain objects that live on the JavaScript heap (which is garbage collected), or are directly owned by objects on the JS…

> I've been arguing lately that C++ should do something like this: Add a full-on theorem-prover to the language so that I can write my own safety rules specific to how my program works. Did you take a look at ATS?

I realize there are obscure programming languages that do this stuff, but I need it in C++.

Re: Jonathan Blow on Rust

#40

Post by crystaldev »

zamalek wrote: post #25

About a year ago I really devoured Jonathan Blow's opinions. He is definitely correct in many, many aspects. I've been paying less and less attention lately because he explains the problems of virtually any language, then explains how his language solves it all perfectly. I am personally incapable of taking firesale arguments like that seriously. I too have many great ideas, but you need to be honest about the limita…

Some people have opinions, Jonathan Blow has opinions by Jonathan Blow.
Post reply on HN