redjamjar

7 ms·

1.
by redjamjar 3y ago
Yeah, ok that’s fair enough!!
2.
by redjamjar 3y ago
I think LLM can help here in various ways. For example, by inferring preconditions/postconditions and loop invariants automatically. Also, perhaps, by writing lemmas as required automatically. I'd guess there has been some work
3.
by redjamjar 3y ago
> I hope this is a typo Yeah, sorry --- that is a typo.
4.
by redjamjar 3y ago
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 unde
5.
by redjamjar 3y ago
> The halting problem has almost no practical relevance because we don't really care about the general case. Yup, agreed
6.
by redjamjar 3y ago
Yeah, SPARK/Ada is a comparable system to Dafny. I agree with that! Also, Frama-C and a bunch of other more esoteric research languages as well.
7.
by redjamjar 3y ago
Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.
8.
by redjamjar 3y ago
> The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating Yeah, look I'm not going to disagree with that. I have had plenty of frustrating time
9.
by redjamjar 3y ago
I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
10.
by redjamjar 3y ago
Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
11.
by redjamjar 3y ago
Haha, yeah ... this one you would have a very hard time with :) Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!
12.
by redjamjar 3y ago
> there are a huge number of useful loops that do useful work and for which you can prove properties like termination Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be ab
13.
Functional Reactive Programming (In Whiley)(youtu.be)
3 points by redjamjar 6y ago|0 comments
14.
Use package managers and dependency declarations? We need your help(massey.au1.qualtrics.com)
3 points by redjamjar 8y ago|0 comments
15.
Neat Demo of Software Verification(youtube.com)
1 points by redjamjar 9y ago|0 comments
16.
What's the Net effect on OOP?(whiley.org)
2 points by redjamjar 9y ago|0 comments
17.
by redjamjar 9y ago
Nice job!! Love the 8 ball example ... really fun :)
18.
Introductory Lecture on Verification in Whiley(whiley.org)
1 points by redjamjar 11y ago|0 comments
19.
The Architecture of Verification in Whiley(whiley.org)
1 points by redjamjar 13y ago|0 comments
20.
Presentation on Whiley [video](whiley.org)
1 points by redjamjar 13y ago|0 comments
21.
VIDEO: Reconstructing 3D Scenes from a Camera [wait for the green car](youtube.com)
4 points by redjamjar 14y ago|1 comments
22.
Understanding Loop Invariants in Whiley(whiley.org)
1 points by redjamjar 14y ago|0 comments
23.
Testing out my Papilio FPGA(whiley.org)
2 points by redjamjar 14y ago|0 comments
24.
Generating Verification Conditions for Whiley(whiley.org)
1 points by redjamjar 14y ago|0 comments
25.
Comparing I/O in C with Java(whiley.org)
1 points by redjamjar 14y ago|0 comments
26.
A Misconception of Functional Programming?(whiley.org)
3 points by redjamjar 14y ago|0 comments
27.
Notes on Java versus C++ Performance(whiley.org)
2 points by redjamjar 14y ago|0 comments
28.
The Liquid Metal Project(whiley.org)
2 points by redjamjar 14y ago|0 comments
29.
Flow Typing for References in Whiley(whiley.org)
1 points by redjamjar 14y ago|0 comments
30.
Writing a PNG Decoder in Whiley(whiley.org)
1 points by redjamjar 15y ago|0 comments

More ›