Conversation

Replying to

sorry for calling you an old fart

Sep 6, 2021

i guess the problem is just scope. considering to move more deliberately to testing. that's where i've found most "tool freedom", and it's a domain that is seriously underestimated

Replying to

there's a lot of interesting stuff going on around formal verification right now

Replying to

anything particular you're thinking of?

Replying to

you should talk to

Replying to

and

wouldn't advise it that guy is crazy

Replying to

and

let's find out

Replying to

and

you know my first response was: i wish i could actually use formal approach in my work. this fermented into: maybe i should just stay away from work where this is not possible

Replying to

and

because if i zoom in to what exactly made last couple of years so difficult, it is all about unpredictable hardware issues. "side problems"

Replying to

and

and overall legacy things that are broken and can't be reasonably fixed

Replying to

and

cant-fix-paint-over infinitely stacking tetris games

6:54 PM · Sep 19, 2021Twitter Web App

Replying to

and

just a heads up spending time in proof assistants is probably the opposite of avoiding "infinitely stacking tetris games"

Replying to

and

and infact, there are people who devote a major portion of their time in improving proof assistants by making the types as tetris-like as possible so that proofs stack more easily

Show replies