🌘 在 Amazon 使用 Dafny 教授程式驗證
➤ 程式驗證教學的新途徑：從證明助理到程式驗證
✤ https://dafny.org/blog/2023/12/15/teaching-program-verification-in-dafny-at-amazon/
Amazon 分享了他們用來教導科學家和工程師程式驗證的教材，包括課程講義和習題。此課程獨特之處在於，它先將 Dafny 視為證明助理獨立教授證明技巧，再引入程式驗證概念。這種方法有助於學習者理解程式驗證背後的邏輯，並在自動驗證失敗時，能更有效地撰寫輔助驗證的斷言。課程分為三個部分：Dafny 程式語言、Dafny 證明助理，以及程式驗證。
+ 這套教材的想法很有趣，先學證明再學驗證，感覺可以更深入地理解程式背後的邏輯。
+ 以前覺得程式驗證很難，看了這個介紹，感覺或許可以嘗試用 Dafny 這套工具來提升程式的可靠性。
#程式驗證 #Dafny #教育 #軟體工程
#Dafny
Teaching Program Verification in Dafny at Amazon (2023)
https://dafny.org/blog/2023/12/15/teaching-program-verification-in-dafny-at-amazon/
#HackerNews #TeachingProgramVerification #Dafny #Amazon #2023 #SoftwareEngineering #CodeQuality
As much as #Dafny intrigues me, the Dev UX is strangely buggy for me. (Trying to hook in an externally written library and every thing is falling apart)
What is worse, the version in Nix appears to be packaged wrongly, (won't recognise dotnet) and I have to resort to binaries from GitHub!
Who da thought! Having multiple distinct uses of `(=)` in your language would be confusing...
For assignment, as a type, and for equations...
Might start not using `(=)` as the type for equality, and use `(===)` more...
Perhaps, for next generation of #Idris , it would be good to have a proper user study on what is appropriate syntax for key aspects of the language.
The strangeness budget for imperative programmers in #CS886 has been blown! The students are warming to #Dafny more! (Rapid introductions aside) The reaction towards the two languages was expected. They do not have a functional, nor PLT background.
I should talk to colleagues about their experience in the other course....
The more I use #Dafny (for teaching) the more I realise that it is, perhaps, too smart and too complex for its own good.
I spent 20+ mins working out how to make a class field private.
20mins reading documentation & a few more minutes fighting syntax.
Whilst, at times, I ain’t the sharpest tool in the box, this does take the cake…
For instance (note I was talking about #Dafny and exploring Design-by-Contract)
The first smart chapter summary:
```
# Exploring Daphne and Emacs Usage
Jan expressed frustration with computers and shared his preference for using Emacs over VS Code. He demonstrated how to use Daphne, a multi-paradigm language, emphasizing its object-oriented and imperative programming capabilities. Jan highlighted that Daphne's main method is where program logic resides and that functions can be side-effect-free. He also mentioned his intention to write a program that computes the absolute value of a number.
```
et voila:
https://github.com/jfdm/skunkworks/tree/main/dafny/4.7.0-stubb
it is not ideal, but it works...
I have managed to get hings working by rolling back to earlier versions.
The bump in #Dafny between 4.7.0 and 4.8.0 hasn't helped either.
Neither is being able to get a single executable generated when running `dafny build`.
#Dafny sadly doesn't have support for #literate_programming a cool feature I think they should support!
Whilst I do not think libraries nor programs should be coded in the literate style, informal presentations and lectures and notes should be!
For #Idris, I have often wrote the presentation in OrgMode and used polymode to mix orgmode and idris-mode together.
Org-mode provides more precision on revealing items and storing reading notes. (one step away from writing that book as well...)
Idris' own mode enables interactive editing.
Key for polymode to work is that the compiler must be literate enabled.
I found a solution through someone's notes on a code sharing platform. Sadly, these notes are not licensed :-(
Not having Reading from STDIN when you can Print to STDIN is not great. #Dafny is not pacman complete.
You need that for shits & giggles, a semi-decent Std Lib too...
#Dafny users, if I wanted to write an interactive program that has a REPL: What support _is_ there for reading from STDIN? The STD library only has file io...
Cursed #dafny I think I need to stop...
```{.dafny}
function fromString(s : string) : Maybe<CMD>
{
bindM(cons(s), (x : (char,string)) =>
if x.0 == ':'
then bindM(cons(words(x.1)), (y : (string, seq<string>)) =>
decide(y.0,y.1))
else Nothing)
}
```
All I wanted was a pure computation context...
Playing with #Dafny (the language) and it’s interesting how there is a mix between pure functional code and imperative code. I cannot, quite, get the idioms or intentions between when I should use imperative over functional. The Functional programmer,l always goes functional…
Reason \((S n)\) as to why I am not fond of #programming #font #ligatures:
+ \(\in\)
+ \(\notin\)
Look the same for me at my usual font size...
#Dafny mode for emacs uses a 'pretty mode' by default (Boo!), worse is that the option is not customisable (BOO!).
```{.elisp}
(defun no-prettification-in-dafny-mode ()
(prettify-symbols-mode -1))
(add-hook 'dafny-mode-hook #'no-prettification-in-dafny-mode)
```
Interesting afternoon playing with #Dafny core concepts. [1]
I am teaching Dafny next semester.
I do not think I will be teaching much much more than the core concepts. (FP, imperative programming, basic proofs, State, Frames, Basic Ghosting), Nothing fancy with ghosts nor proofs nor OO.
Just too much to do in a course with the audience I *think* I have. (Some people like to push students hard; I do not)
I also think I wll go against my gut and lecture half with slides (overview and paradigms) and half live coding (explore the fundamentals).
Revisiting thinking of using #stacscheck [1] for #goldenfile testing of projects.
The language of assessment (#dafny) doesn't seem to do goldenfile testing 'out-of-the-box', and internal unit-testing is not what I 'want'.
Sadly, I wasn't aware of the `lit` program [2] which _was_ used by dafny, and so not available on lab machines.
Tempting to revisit and extend a haskell based setup derived from Idris(1) test suite I used when at Glasgow, or co-opt idris2's test suite for it all...
Teaching is fun...
[1] https://github.com/ChrisJefferson/stacscheck
[2] https://llvm.org/docs/CommandGuide/lit.html
#Dafny users, is there a standard way to perform 'whole program' golden file testing of dafny executables?
That is, I want a suite of tests to pass input to a program and compare output with expected output. As we do in Idris2 https://github.com/idris-lang/Idris2/tree/main/tests
Client Info
Server: https://mastodon.social
Version: 2025.04
Repository: https://github.com/cyevgeniy/lmst