Programming Languages Going Above and Beyond

Re:Programming Languages Going Above and Beyond by fjfaase on Thursday June 29, 2023 @11:23AM (#36521655)

This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain.

A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct.

[1] https://www.iwriteiam.nl/AoP.html

[ Parent | on HN ]

Re:Programming Languages Going Above and Beyond by skydhash on Thursday June 29, 2023 @11:28AM (#36521742)

You may want to do a Find and Replace (piramid to pyramid).

[ Parent | on HN ]

Re:Programming Languages Going Above and Beyond by redjamjar on Thursday June 29, 2023 @05:30PM (#36527014)

So, you can use fixed-width data types in Dafny and verify properties about functions using them. For example, in our EVM implementation we have types like u8, u16, u256, etc. Of course, Dafny won't let operations on these types underflow or overflow, so it does mean more work ensuring your code doesn't allow this.

[ Parent | on HN ]